max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: use <|

Browse source
This commit is contained in:
Leonardo de Moura 2020-11-19 09:03:38 -08:00
parent b6a1914299
commit 304c80d610
23 changed files with 164 additions and 160 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Init/Classical.lean
View file

@ -15,7 +15,7 @@ namespace Classical
axiom choice {α : Sort u} : Nonempty α → α
noncomputable def indefiniteDescription {α : Sort u} (p : α → Prop) (h : Exists (fun x => p x)) : {x // p x} :=
choice $ let ⟨x, px⟩ := h; ⟨⟨x, px⟩⟩
choice <| let ⟨x, px⟩ := h; ⟨⟨x, px⟩⟩
noncomputable def choose {α : Sort u} {p : α → Prop} (h : Exists (fun x => p x)) : α :=
(indefiniteDescription p h).val
@ -68,7 +68,7 @@ noncomputable def inhabitedOfExists {α : Sort u} {p : α → Prop} (h : Exists
/- all propositions are Decidable -/
noncomputable def propDecidable (a : Prop) : Decidable a :=
choice $ match em a with
choice <| match em a with
| Or.inl h => ⟨isTrue h⟩
| Or.inr h => ⟨isFalse h⟩

2
src/Init/Coe.lean
View file

@ -148,4 +148,4 @@ instance hasOfNatOfCoe {α : Type u} {β : Type v} [OfNat α] [Coe α β] : OfNa
@[inline] def coeM {m : Type u → Type v} {α β : Type u} [∀ a, CoeT α a β] [Monad m] (x : m α) : m β := do
let a ← x
pure $ coe a
pure <| coe a

30
src/Init/Control/Except.lean
View file

@ -35,10 +35,10 @@ variables {ε : Type u}
@[inline] protected def map {α β : Type v} (f : α → β) : Except ε α → Except ε β
| Except.error err => Except.error err
| Except.ok v => Except.ok $ f v
| Except.ok v => Except.ok <| f v
@[inline] protected def mapError {ε' : Type u} {α : Type v} (f : ε → ε') : Except ε α → Except ε' α
| Except.error err => Except.error $ f err
| Except.error err => Except.error <| f err
| Except.ok v => Except.ok v
@[inline] protected def bind {α β : Type v} (ma : Except ε α) (f : α → Except ε β) : Except ε β :=
@ -78,28 +78,28 @@ namespace ExceptT
variables {ε : Type u} {m : Type u → Type v} [Monad m]
@[inline] protected def pure {α : Type u} (a : α) : ExceptT ε m α :=
ExceptT.mk $ pure (Except.ok a)
ExceptT.mk <| pure (Except.ok a)
@[inline] protected def bindCont {α β : Type u} (f : α → ExceptT ε m β) : Except ε α → m (Except ε β)
| Except.ok a => f a
| Except.error e => pure (Except.error e)
@[inline] protected def bind {α β : Type u} (ma : ExceptT ε m α) (f : α → ExceptT ε m β) : ExceptT ε m β :=
ExceptT.mk $ ma >>= ExceptT.bindCont f
ExceptT.mk <| ma >>= ExceptT.bindCont f
@[inline] protected def map {α β : Type u} (f : α → β) (x : ExceptT ε m α) : ExceptT ε m β :=
ExceptT.mk $ x >>= fun a => match a with
| (Except.ok a) => pure $ Except.ok (f a)
| (Except.error e) => pure $ Except.error e
ExceptT.mk <| x >>= fun a => match a with
| (Except.ok a) => pure <| Except.ok (f a)
| (Except.error e) => pure <| Except.error e
@[inline] protected def lift {α : Type u} (t : m α) : ExceptT ε m α :=
ExceptT.mk $ Except.ok <$> t
ExceptT.mk <| Except.ok <$> t
instance : MonadLift (Except ε) (ExceptT ε m) := ⟨fun e => ExceptT.mk $ pure e⟩
instance : MonadLift (Except ε) (ExceptT ε m) := ⟨fun e => ExceptT.mk <| pure e⟩
instance : MonadLift m (ExceptT ε m) := ⟨ExceptT.lift⟩
@[inline] protected def tryCatch {α : Type u} (ma : ExceptT ε m α) (handle : ε → ExceptT ε m α) : ExceptT ε m α :=
ExceptT.mk $ ma >>= fun res => match res with
ExceptT.mk <| ma >>= fun res => match res with
| Except.ok a => pure (Except.ok a)
| Except.error e => (handle e)
@ -112,17 +112,17 @@ instance : Monad (ExceptT ε m) := {
}
@[inline] protected def adapt {ε' α : Type u} (f : ε → ε') : ExceptT ε m α → ExceptT ε' m α := fun x =>
ExceptT.mk $ Except.mapError f <$> x
ExceptT.mk <| Except.mapError f <$> x
end ExceptT
instance (m : Type u → Type v) (ε₁ : Type u) (ε₂ : Type u) [Monad m] [MonadExceptOf ε₁ m] : MonadExceptOf ε₁ (ExceptT ε₂ m) := {
throw := fun e => ExceptT.mk $ throwThe ε₁ e,
tryCatch := fun x handle => ExceptT.mk $ tryCatchThe ε₁ x handle
throw := fun e => ExceptT.mk <| throwThe ε₁ e,
tryCatch := fun x handle => ExceptT.mk <| tryCatchThe ε₁ x handle
}
instance (m : Type u → Type v) (ε : Type u) [Monad m] : MonadExceptOf ε (ExceptT ε m) := {
throw := fun e => ExceptT.mk $ pure (Except.error e),
throw := fun e => ExceptT.mk <| pure (Except.error e),
tryCatch := ExceptT.tryCatch
}
@ -146,7 +146,7 @@ end MonadExcept
instance (ε : Type u) (m : Type u → Type v) [Monad m] : MonadControl m (ExceptT ε m) := {
stM := Except ε,
liftWith := fun f => liftM $ f fun x => x.run,
liftWith := fun f => liftM <| f fun x => x.run,
restoreM := fun x => x
}

6
src/Init/Core.lean
View file

@ -306,7 +306,7 @@ theorem Exists.elim {α : Sort u} {p : α → Prop} {b : Prop}
theorem decideTrueEqTrue (h : Decidable True) : @decide True h = true :=
match h with
| isTrue h => rfl
| isFalse h => False.elim $ h ⟨⟩
| isFalse h => False.elim <| h ⟨⟩
theorem decideFalseEqFalse (h : Decidable False) : @decide False h = false :=
match h with
@ -758,7 +758,7 @@ protected abbrev hrecOn
(f : (a : α) → motive (Quot.mk r a))
(c : (a b : α) → (p : r a b) → f a ≅ f b)
: motive q :=
Quot.recOn q f fun a b p => eqOfHEq $
Quot.recOn q f fun a b p => eqOfHEq <|
have p₁ : Eq.ndrec (f a) (sound p) ≅ f a := eqRecHEq (sound p) (f a)
HEq.trans p₁ (c a b p)
@ -977,7 +977,7 @@ variables {α : Sort u} {β : α → Sort v}
private def funSetoid (α : Sort u) (β : α → Sort v) : Setoid (∀ (x : α), β x) :=
Setoid.mk (@Function.Equiv α β) (Function.Equiv.isEquivalence α β)
private def extfunApp (f : Quotient $ funSetoid α β) (x : α) : β x :=
private def extfunApp (f : Quotient <| funSetoid α β) (x : α) : β x :=
Quot.liftOn f
(fun (f : ∀ (x : α), β x) => f x)
(fun f₁ f₂ h => h x)

38
src/Init/Data/Array/Basic.lean
View file

@ -120,13 +120,13 @@ def modifyM {m : Type u → Type v} [Monad m] [Inhabited α] (a : Array α) (i :
let v := a.get idx
let a' := a.set idx (arbitrary α)
let v ← f v
pure $ (a'.set (sizeSetEq a .. ▸ idx) v)
pure <| a'.set (sizeSetEq a .. ▸ idx) v
else
pure a
@[inline]
def modify [Inhabited α] (a : Array α) (i : Nat) (f : α → α) : Array α :=
Id.run $ a.modifyM i f
Id.run <| a.modifyM i f
@[inline]
def modifyOp [Inhabited α] (self : Array α) (idx : Nat) (f : α → α) : Array α :=
@ -255,7 +255,7 @@ unsafe def mapMUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad
map (i+1) (r.uset i (unsafeCast vNew) lcProof)
else
pure (unsafeCast r)
unsafeCast $ map 0 (unsafeCast as)
unsafeCast <| map 0 (unsafeCast as)
/- Reference implementation for `mapM` -/
@[implementedBy mapMUnsafe]
@ -368,27 +368,27 @@ def forRevM {α : Type u} {m : Type v → Type w} [Monad m] (f : α → m PUnit)
@[inline]
def foldl {α : Type u} {β : Type v} (f : β → α → β) (init : β) (as : Array α) (start := 0) (stop := as.size) : β :=
Id.run $ as.foldlM f init start stop
Id.run <| as.foldlM f init start stop
@[inline]
def foldr {α : Type u} {β : Type v} (f : α → β → β) (init : β) (as : Array α) (start := as.size) (stop := 0) : β :=
Id.run $ as.foldrM f init start stop
Id.run <| as.foldrM f init start stop
@[inline]
def map {α : Type u} {β : Type v} (f : α → β) (as : Array α) : Array β :=
Id.run $ as.mapM f
Id.run <| as.mapM f
@[inline]
def mapIdx {α : Type u} {β : Type v} (as : Array α) (f : Fin as.size → α → β) : Array β :=
Id.run $ as.mapIdxM f
Id.run <| as.mapIdxM f
@[inline]
def find? {α : Type} (as : Array α) (p : α → Bool) : Option α :=
Id.run $ as.findM? p
Id.run <| as.findM? p
@[inline]
def findSome? {α : Type u} {β : Type v} (as : Array α) (f : α → Option β) : Option β :=
Id.run $ as.findSomeM? f
Id.run <| as.findSomeM? f
@[inline]
def findSome! {α : Type u} {β : Type v} [Inhabited β] (a : Array α) (f : α → Option β) : β :=
@ -398,11 +398,11 @@ def findSome! {α : Type u} {β : Type v} [Inhabited β] (a : Array α) (f : α
@[inline]
def findSomeRev? {α : Type u} {β : Type v} (as : Array α) (f : α → Option β) : Option β :=
Id.run $ as.findSomeRevM? f
Id.run <| as.findSomeRevM? f
@[inline]
def findRev? {α : Type} (as : Array α) (p : α → Bool) : Option α :=
Id.run $ as.findRevM? p
Id.run <| as.findRevM? p
@[inline]
def findIdx? {α : Type u} (as : Array α) (p : α → Bool) : Option Nat :=
@ -430,11 +430,11 @@ a.findIdx? fun a => a == v
@[inline]
def any {α : Type u} (p : α → Bool) (as : Array α) (start := 0) (stop := as.size) : Bool :=
Id.run $ as.anyM p start stop
Id.run <| as.anyM p start stop
@[inline]
def all {α : Type u} (p : α → Bool) (as : Array α) (start := 0) (stop := as.size) : Bool :=
Id.run $ as.allM p start stop
Id.run <| as.allM p start stop
def contains {α} [BEq α] (as : Array α) (a : α) : Bool :=
as.any fun b => a == b
@ -454,7 +454,7 @@ partial def reverse {α : Type u} (as : Array α) : Array α :=
rev as 0
@[inline] def getEvenElems {α : Type u} (as : Array α) : Array α :=
(·.2) $ as.foldl (init := (true, Array.empty)) fun (even, r) a =>
(·.2) <| as.foldl (init := (true, Array.empty)) fun (even, r) a =>
if even then
(false, r.push a)
else
@ -540,13 +540,13 @@ def filterMapM {m : Type u → Type v} [Monad m] {α β : Type u} (f : α → m
@[inline]
def filterMap {α β : Type u} (f : α → Option β) (as : Array α) (start := 0) (stop := as.size) : Array β :=
Id.run $ as.filterMapM f (start := start) (stop := stop)
Id.run <| as.filterMapM f (start := start) (stop := stop)
@[specialize]
def getMax? {α : Type u} (as : Array α) (lt : α → α → Bool) : Option α :=
if h : 0 < as.size then
let a0 := as.get ⟨0, h⟩
some $ as.foldl (init := a0) (start := 1) fun best a =>
some <| as.foldl (init := a0) (start := 1) fun best a =>
if lt best a then a else best
else
none
@ -688,7 +688,7 @@ def toListLitAux {α : Type u} (a : Array α) (n : Nat) (hsz : a.size = n) : ∀
| (i+1), hi, acc => toListLitAux a n hsz i (Nat.leOfSuccLe hi) (a.getLit i hsz (Nat.ltOfLtOfEq (Nat.ltOfLtOfLe (Nat.ltSuccSelf i) hi) hsz) :: acc)
def toArrayLit {α : Type u} (a : Array α) (n : Nat) (hsz : a.size = n) : Array α :=
List.toArray $ toListLitAux a n hsz n (hsz ▸ Nat.leRefl _) []
List.toArray <| toListLitAux a n hsz n (hsz ▸ Nat.leRefl _) []
theorem toArrayLitEq {α : Type u} (a : Array α) (n : Nat) (hsz : a.size = n) : a = toArrayLit a n hsz :=
-- TODO: this is painful to prove without proper automation
@ -728,7 +728,7 @@ theorem toArrayLitEq {α : Type u} (a : Array α) (n : Nat) (hsz : a.size = n) :
- (toListLitAux a n hsz n _ []).length = n
- j < n -> (List.toArray as).getLit j _ _ = as.index j
Then using Array.extLit, we have that a = List.toArray $ toListLitAux a n hsz n _ []
Then using Array.extLit, we have that a = List.toArray <| toListLitAux a n hsz n _ []
-/
partial def isPrefixOfAux {α : Type u} [BEq α] (as bs : Array α) (hle : as.size ≤ bs.size) : Nat → Bool
@ -772,7 +772,7 @@ def allDiff {α} [BEq α] (as : Array α) : Bool :=
let a := as.get ⟨i, h⟩;
if h : i < bs.size then
let b := bs.get ⟨i, h⟩;
zipWithAux f as bs (i+1) (cs.push $ f a b)
zipWithAux f as bs (i+1) <| cs.push <| f a b
else
cs
else

16
src/Init/Data/Array/BinSearch.lean
View file

@ -42,12 +42,12 @@ namespace Array
let mid := (lo + hi)/2;
let midVal := as.get! mid;
if lt midVal k then
if mid == lo then do let v ← add (); pure $ as.insertAt (lo+1) v
if mid == lo then do let v ← add (); pure <| as.insertAt (lo+1) v
else binInsertAux lt merge add as k mid hi
else if lt k midVal then
binInsertAux lt merge add as k lo mid
else do
as.modifyM mid $ fun v => merge v
as.modifyM mid <| fun v => merge v
@[specialize] partial def binInsertM {α : Type u} {m : Type u → Type v} [Monad m] [Inhabited α]
(lt : α → α → Bool)
@ -55,14 +55,14 @@ namespace Array
(add : Unit → m α)
(as : Array α)
(k : α) : m (Array α) :=
if as.isEmpty then do let v ← add (); pure $ as.push v
else if lt k (as.get! 0) then do let v ← add (); pure $ as.insertAt 0 v
else if !lt (as.get! 0) k then as.modifyM 0 $ merge
else if lt as.back k then do let v ← add (); pure $ as.push v
else if !lt k as.back then as.modifyM (as.size - 1) $ merge
if as.isEmpty then do let v ← add (); pure <| as.push v
else if lt k (as.get! 0) then do let v ← add (); pure <| as.insertAt 0 v
else if !lt (as.get! 0) k then as.modifyM 0 <| merge
else if lt as.back k then do let v ← add (); pure <| as.push v
else if !lt k as.back then as.modifyM (as.size - 1) <| merge
else binInsertAux lt merge add as k 0 (as.size - 1)
@[inline] def binInsert {α : Type u} [Inhabited α] (lt : α → α → Bool) (as : Array α) (k : α) : Array α :=
Id.run $ binInsertM lt (fun _ => k) (fun _ => k) as k
Id.run <| binInsertM lt (fun _ => k) (fun _ => k) as k
end Array

8
src/Init/Data/Array/Subarray.lean
View file

@ -60,19 +60,19 @@ def forRevM {α : Type u} {m : Type v → Type w} [Monad m] (f : α → m PUnit)
@[inline]
def foldl {α : Type u} {β : Type v} (f : β → α → β) (init : β) (as : Subarray α) : β :=
Id.run $ as.foldlM f (init := init)
Id.run <| as.foldlM f (init := init)
@[inline]
def foldr {α : Type u} {β : Type v} (f : α → β → β) (init : β) (as : Subarray α) : β :=
Id.run $ as.foldrM f (init := init)
Id.run <| as.foldrM f (init := init)
@[inline]
def any {α : Type u} (p : α → Bool) (as : Subarray α) : Bool :=
Id.run $ as.anyM p
Id.run <| as.anyM p
@[inline]
def all {α : Type u} (p : α → Bool) (as : Subarray α) : Bool :=
Id.run $ as.allM p
Id.run <| as.allM p
end Subarray

18
src/Init/Data/Int/Basic.lean
View file

@ -86,13 +86,13 @@ set_option bootstrap.gen_matcher_code false in
protected def decEq (a b : @& Int) : Decidable (a = b) :=
match a, b with
| ofNat a, ofNat b => match decEq a b with
| isTrue h => isTrue $ h ▸ rfl
| isFalse h => isFalse $ fun h' => Int.noConfusion h' (fun h' => absurd h' h)
| isTrue h => isTrue <| h ▸ rfl
| isFalse h => isFalse <| fun h' => Int.noConfusion h' (fun h' => absurd h' h)
| negSucc a, negSucc b => match decEq a b with
| isTrue h => isTrue $ h ▸ rfl
| isFalse h => isFalse $ fun h' => Int.noConfusion h' (fun h' => absurd h' h)
| ofNat a, negSucc b => isFalse $ fun h => Int.noConfusion h
| negSucc a, ofNat b => isFalse $ fun h => Int.noConfusion h
| isTrue h => isTrue <| h ▸ rfl
| isFalse h => isFalse <| fun h' => Int.noConfusion h' (fun h' => absurd h' h)
| ofNat a, negSucc b => isFalse <| fun h => Int.noConfusion h
| negSucc a, ofNat b => isFalse <| fun h => Int.noConfusion h
instance : DecidableEq Int := Int.decEq
@ -100,8 +100,8 @@ set_option bootstrap.gen_matcher_code false in
@[extern "lean_int_dec_nonneg"]
private def decNonneg (m : @& Int) : Decidable (NonNeg m) :=
match m with
| ofNat m => isTrue $ NonNeg.mk m
| negSucc m => isFalse $ fun h => nomatch h
| ofNat m => isTrue <| NonNeg.mk m
| negSucc m => isFalse <| fun h => nomatch h
@[extern "lean_int_dec_le"]
instance decLe (a b : @& Int) : Decidable (a ≤ b) :=
@ -156,7 +156,7 @@ namespace String
def toInt? (s : String) : Option Int :=
if s.get 0 = '-' then do
let v ← (s.toSubstring.drop 1).toNat?;
pure $ - Int.ofNat v
pure <| - Int.ofNat v
else
Int.ofNat <$> s.toNat?

2
src/Init/Data/Nat/Basic.lean
View file

@ -297,7 +297,7 @@ protected theorem addLeAddLeft {n m : Nat} (h : n ≤ m) (k : Nat) : k + n ≤ k
| ⟨w, hw⟩ =>
have h₁ : k + n + w = k + (n + w) from Nat.addAssoc ..
have h₂ : k + (n + w) = k + m from congrArg _ hw
le.intro $ h₁.trans h₂
le.intro <| h₁.trans h₂
protected theorem addLeAddRight {n m : Nat} (h : n ≤ m) (k : Nat) : n + k ≤ m + k := by
rw [Nat.addComm n k, Nat.addComm m k]

6
src/Init/Data/Repr.lean
View file

@ -93,7 +93,7 @@ def digitChar (n : Nat) : Char :=
def toDigitsCore (base : Nat) : Nat → Nat → List Char → List Char
| 0, n, ds => ds
| fuel+1, n, ds =>
let d := digitChar $ n % base;
let d := digitChar <| n % base;
let n' := n / base;
if n' = 0 then d::ds
else toDigitsCore base fuel n' (d::ds)
@ -119,7 +119,7 @@ def superDigitChar (n : Nat) : Char :=
partial def toSuperDigitsAux : Nat → List Char → List Char
| n, ds =>
let d := superDigitChar $ n % 10;
let d := superDigitChar <| n % 10;
let n' := n / 10;
if n' = 0 then d::ds
else toSuperDigitsAux n' (d::ds)
@ -136,7 +136,7 @@ instance : Repr Nat :=
⟨Nat.repr⟩
def hexDigitRepr (n : Nat) : String :=
String.singleton $ Nat.digitChar n
String.singleton <| Nat.digitChar n
def charToHex (c : Char) : String :=
let n := Char.toNat c;

12
src/Init/Data/String/Basic.lean
View file

@ -64,7 +64,7 @@ def set : String → (@& Pos) → Char → String
| ⟨s⟩, i, c => ⟨utf8SetAux c s 0 i⟩
def modify (s : String) (i : Pos) (f : Char → Char) : String :=
s.set i $ f $ s.get i
s.set i <| f <| s.get i
@[extern "lean_string_utf8_next"]
def next (s : @& String) (p : @& Pos) : Pos :=
@ -295,11 +295,11 @@ s.any (fun a => a == c)
mapAux f 0 s
def isNat (s : String) : Bool :=
s.all $ fun c => c.isDigit
s.all fun c => c.isDigit
def toNat? (s : String) : Option Nat :=
if s.isNat then
some $ s.foldl (fun n c => n*10 + (c.toNat - '0'.toNat)) 0
some <| s.foldl (fun n c => n*10 + (c.toNat - '0'.toNat)) 0
else
none
@ -456,11 +456,11 @@ def contains (s : Substring) (c : Char) : Bool :=
⟨s, b, e⟩
def isNat (s : Substring) : Bool :=
s.all $ fun c => c.isDigit
s.all fun c => c.isDigit
def toNat? (s : Substring) : Option Nat :=
if s.isNat then
some $ s.foldl (fun n c => n*10 + (c.toNat - '0'.toNat)) 0
some <| s.foldl (fun n c => n*10 + (c.toNat - '0'.toNat)) 0
else
none
@ -507,7 +507,7 @@ def trim (s : String) : String :=
nextWhile s (fun c => !p c) i
def capitalize (s : String) :=
s.set 0 $ (s.get 0).toUpper
s.set 0 <| s.get 0 |>.toUpper
end String

37
src/Init/Meta.lean
View file

@ -116,20 +116,21 @@ partial def getTailInfo : Syntax → Option SourceInfo
| _ => none
@[specialize] private partial def updateLast {α} [Inhabited α] (a : Array α) (f : α → Option α) (i : Nat) : Option (Array α) :=
if i == 0 then none
if i == 0 then
none
else
let i := i - 1;
let v := a.get! i;
let i := i - 1
let v := a[i]
match f v with
| some v => some $ a.set! i v
| some v => some <| a.set! i v
| none => updateLast a f i
partial def setTailInfoAux (info : SourceInfo) : Syntax → Option Syntax
| atom _ val => some $ atom info val
| ident _ rawVal val pre => some $ ident info rawVal val pre
| atom _ val => some <| atom info val
| ident _ rawVal val pre => some <| ident info rawVal val pre
| node k args =>
match updateLast args (setTailInfoAux info) args.size with
| some args => some $ node k args
| some args => some <| node k args
| none => none
| stx => none
@ -147,17 +148,17 @@ def unsetTrailing (stx : Syntax) : Syntax :=
if h : i < a.size then
let v := a.get ⟨i, h⟩;
match f v with
| some v => some $ a.set ⟨i, h⟩ v
| some v => some <| a.set ⟨i, h⟩ v
| none => updateFirst a f (i+1)
else
none
partial def setHeadInfoAux (info : SourceInfo) : Syntax → Option Syntax
| atom _ val => some $ atom info val
| ident _ rawVal val pre => some $ ident info rawVal val pre
| atom _ val => some <| atom info val
| ident _ rawVal val pre => some <| ident info rawVal val pre
| node k args =>
match updateFirst args (setHeadInfoAux info) 0 with
| some args => some $ node k args
| some args => some <| node k args
| noxne => none
| stx => none
@ -172,7 +173,7 @@ def setInfo (info : SourceInfo) : Syntax → Syntax
| stx => stx
partial def replaceInfo (info : SourceInfo) : Syntax → Syntax
| node k args => node k $ args.map (replaceInfo info)
| node k args => node k <| args.map (replaceInfo info)
| stx => setInfo info stx
def copyInfo (s : Syntax) (source : Syntax) : Syntax :=
@ -204,8 +205,8 @@ partial def expandMacros : Syntax → MacroM Syntax
match (← expandMacro? stx) with
| some stxNew => expandMacros stxNew
| none => do
let args ← Macro.withIncRecDepth stx $ args.mapM expandMacros
pure $ Syntax.node k args
let args ← Macro.withIncRecDepth stx <| args.mapM expandMacros
pure <| Syntax.node k args
| stx => pure stx
/- Helper functions for processing Syntax programmatically -/
@ -268,7 +269,7 @@ def mkHole (ref : Syntax) : Syntax :=
namespace Syntax
def mkSep (a : Array Syntax) (sep : Syntax) : Syntax :=
mkNullNode $ mkSepArray a sep
mkNullNode <| mkSepArray a sep
/-- Create syntax representing a Lean term application, but avoid degenerate empty applications. -/
def mkApp (fn : Syntax) : (args : Array Syntax) → Syntax
@ -533,7 +534,7 @@ export Quote (quote)
instance : Quote Syntax := ⟨id⟩
instance : Quote Bool := ⟨fun | true => mkCIdent `Bool.true | false => mkCIdent `Bool.false⟩
instance : Quote String := ⟨Syntax.mkStrLit⟩
instance : Quote Nat := ⟨fun n => Syntax.mkNumLit $ toString n⟩
instance : Quote Nat := ⟨fun n => Syntax.mkNumLit <| toString n⟩
instance : Quote Substring := ⟨fun s => Syntax.mkCApp `String.toSubstring #[quote s.toString]⟩
private def quoteName : Name → Syntax
@ -590,7 +591,7 @@ def filterSepElemsM {m : Type → Type} [Monad m] (a : Array Syntax) (p : Syntax
filterSepElemsMAux a p 0 #[]
def filterSepElems (a : Array Syntax) (p : Syntax → Bool) : Array Syntax :=
Id.run $ a.filterSepElemsM p
Id.run <| a.filterSepElemsM p
private partial def mapSepElemsMAux {m : Type → Type} [Monad m] (a : Array Syntax) (f : Syntax → m Syntax) (i : Nat) (acc : Array Syntax) : m (Array Syntax) := do
if h : i < a.size then
@ -607,7 +608,7 @@ def mapSepElemsM {m : Type → Type} [Monad m] (a : Array Syntax) (f : Syntax
mapSepElemsMAux a f 0 #[]
def mapSepElems (a : Array Syntax) (f : Syntax → Syntax) : Array Syntax :=
Id.run $ a.mapSepElemsM f
Id.run <| a.mapSepElemsM f
end Array

43
src/Init/System/IO.lean
View file

@ -200,7 +200,7 @@ def Handle.write (h : Handle) (s : ByteArray) : m Unit := liftM (Prim.Handle.wri
def Handle.getLine : Handle → m String := liftM ∘ Prim.Handle.getLine
def Handle.putStr (h : Handle) (s : String) : m Unit :=
liftM $ Prim.Handle.putStr h s
liftM <| Prim.Handle.putStr h s
def Handle.putStrLn (h : Handle) (s : String) : m Unit :=
h.putStr (s.push '\n')
@ -226,9 +226,9 @@ partial def lines (fname : String) : m (Array String) := do
else if line.back == '\n' then
let line := line.dropRight 1
let line := if System.Platform.isWindows && line.back == '\x0d' then line.dropRight 1 else line
read $ lines.push line
read <| lines.push line
else
pure $ lines.push line
pure <| lines.push line
read #[]
@ -259,29 +259,32 @@ def setStderr : FS.Stream → m FS.Stream := liftM ∘ Prim.setStderr
def withStdin [MonadFinally m] {α} (h : FS.Stream) (x : m α) : m α := do
let prev ← setStdin h
try x finally discard $ setStdin prev
try x finally discard <| setStdin prev
def withStdout [MonadFinally m] {α} (h : FS.Stream) (x : m α) : m α := do
let prev ← setStdout h
try x finally discard $ setStdout prev
try
x
finally
discard <| setStdout prev
def withStderr [MonadFinally m] {α} (h : FS.Stream) (x : m α) : m α := do
let prev ← setStderr h
try x finally discard $ setStderr prev
try x finally discard <| setStderr prev
def print {α} [ToString α] (s : α) : IO Unit := do
let out ← getStdout
out.putStr $ toString s
out.putStr <| toString s
def println {α} [ToString α] (s : α) : IO Unit :=
print ((toString s).push '\n')
def eprint {α} [ToString α] (s : α) : IO Unit := do
let out ← getStderr
liftM $ out.putStr $ toString s
liftM <| out.putStr <| toString s
def eprintln {α} [ToString α] (s : α) : IO Unit :=
eprint ((toString s).push '\n')
eprint <| toString s |>.push '\n'
@[export lean_io_eprintln]
private def eprintlnAux (s : String) : IO Unit :=
@ -358,7 +361,7 @@ def output (args : SpawnArgs) : IO Output := do
def run (args : SpawnArgs) : IO String := do
let out ← output args
if out.exitCode != 0 then
throw $ IO.userError $ "process '" ++ args.cmd ++ "' exited with code " ++ toString out.exitCode;
throw <| IO.userError <| "process '" ++ args.cmd ++ "' exited with code " ++ toString out.exitCode;
pure out.stdout
end Process
@ -370,7 +373,7 @@ def AccessRight.flags (acc : AccessRight) : UInt32 :=
let r : UInt32 := if acc.read then 0x4 else 0
let w : UInt32 := if acc.write then 0x2 else 0
let x : UInt32 := if acc.execution then 0x1 else 0
r.lor $ w.lor x
r.lor <| w.lor x
structure FileRight :=
(user group other : AccessRight := { })
@ -379,7 +382,7 @@ def FileRight.flags (acc : FileRight) : UInt32 :=
let u : UInt32 := acc.user.flags.shiftLeft 6
let g : UInt32 := acc.group.flags.shiftLeft 3
let o : UInt32 := acc.other.flags
u.lor $ g.lor o
u.lor <| g.lor o
@[extern "lean_chmod"] constant Prim.setAccessRights (filename : @& String) (mode : UInt32) : IO Unit
@ -415,7 +418,7 @@ structure Buffer :=
(pos : Nat := 0)
def ofBuffer (r : Ref Buffer) : Stream := {
isEof := do let b ← r.get; pure $ b.pos >= b.data.size,
isEof := do let b ← r.get; pure <| b.pos >= b.data.size,
flush := pure (),
read := fun n => r.modifyGet fun b =>
let data := b.data.extract b.pos (b.pos + n.toNat)
@ -425,10 +428,10 @@ def ofBuffer (r : Ref Buffer) : Stream := {
{ b with data := data.copySlice 0 b.data b.pos data.size false, pos := b.pos + data.size },
getLine := r.modifyGet fun b =>
let pos := match b.data.findIdx? (start := b.pos) fun u => u == 0 || u = '\n'.toNat.toUInt8 with
-- include '\n', but not '\0'
| some pos => if b.data.get! pos == 0 then pos else pos + 1
| none => b.data.size
(String.fromUTF8Unchecked $ b.data.extract b.pos pos, { b with pos := pos }),
-- include '\n', but not '\0'
| some pos => if b.data.get! pos == 0 then pos else pos + 1
| none => b.data.size
(String.fromUTF8Unchecked <| b.data.extract b.pos pos, { b with pos := pos }),
putStr := fun s => r.modify fun b =>
let data := s.toUTF8
{ b with data := data.copySlice 0 b.data b.pos data.size false, pos := b.pos + data.size },
@ -439,9 +442,9 @@ end Stream
def withIsolatedStreams {α : Type} (x : IO α) : IO (String × Except IO.Error α) := do
let bIn ← mkRef { : Stream.Buffer }
let bOut ← mkRef { : Stream.Buffer }
let r ← withStdin (Stream.ofBuffer bIn) $
withStdout (Stream.ofBuffer bOut) $
withStderr (Stream.ofBuffer bOut) $
let r ← withStdin (Stream.ofBuffer bIn) <|
withStdout (Stream.ofBuffer bOut) <|
withStderr (Stream.ofBuffer bOut) <|
observing x
let bOut ← bOut.get
let out := String.fromUTF8Unchecked bOut.data

20
src/Init/System/ST.lean
View file

@ -46,7 +46,7 @@ structure Ref (σ : Type) (α : Type) : Type :=
(ref : RefPointed.type) (h : Nonempty α)
instance {σ α} [Inhabited α] : Inhabited (Ref σ α) :=
⟨{ ref := RefPointed.val, h := Nonempty.intro $ arbitrary _}⟩
⟨{ ref := RefPointed.val, h := Nonempty.intro <| arbitrary _}⟩
namespace Prim
@ -54,7 +54,7 @@ set_option pp.all true
/- Auxiliary definition for showing that `ST σ α` is inhabited when we have a `Ref σ α` -/
private noncomputable def inhabitedFromRef {σ α} (r : Ref σ α) : ST σ α :=
let inh : Inhabited α := Classical.inhabitedOfNonempty r.h
pure $ arbitrary α
pure <| arbitrary α
@[extern "lean_st_mk_ref"]
constant mkRef {σ α} (a : α) : ST σ (Ref σ α) := pure { ref := RefPointed.val, h := Nonempty.intro a }
@ -96,14 +96,14 @@ end Prim
section
variables {σ : Type} {m : Type → Type} [Monad m] [MonadLiftT (ST σ) m]
@[inline] def mkRef {α : Type} (a : α) : m (Ref σ α) := liftM $ Prim.mkRef a
@[inline] def Ref.get {α : Type} (r : Ref σ α) : m α := liftM $ Prim.Ref.get r
@[inline] def Ref.set {α : Type} (r : Ref σ α) (a : α) : m Unit := liftM $ Prim.Ref.set r a
@[inline] def Ref.swap {α : Type} (r : Ref σ α) (a : α) : m α := liftM $ Prim.Ref.swap r a
@[inline] unsafe def Ref.take {α : Type} (r : Ref σ α) : m α := liftM $ Prim.Ref.take r
@[inline] def Ref.ptrEq {α : Type} (r1 r2 : Ref σ α) : m Bool := liftM $ Prim.Ref.ptrEq r1 r2
@[inline] def Ref.modify {α : Type} (r : Ref σ α) (f : α → α) : m Unit := liftM $ Prim.Ref.modify r f
@[inline] def Ref.modifyGet {α : Type} {β : Type} (r : Ref σ α) (f : α → β × α) : m β := liftM $ Prim.Ref.modifyGet r f
@[inline] def mkRef {α : Type} (a : α) : m (Ref σ α) := liftM <| Prim.mkRef a
@[inline] def Ref.get {α : Type} (r : Ref σ α) : m α := liftM <| Prim.Ref.get r
@[inline] def Ref.set {α : Type} (r : Ref σ α) (a : α) : m Unit := liftM <| Prim.Ref.set r a
@[inline] def Ref.swap {α : Type} (r : Ref σ α) (a : α) : m α := liftM <| Prim.Ref.swap r a
@[inline] unsafe def Ref.take {α : Type} (r : Ref σ α) : m α := liftM <| Prim.Ref.take r
@[inline] def Ref.ptrEq {α : Type} (r1 r2 : Ref σ α) : m Bool := liftM <| Prim.Ref.ptrEq r1 r2
@[inline] def Ref.modify {α : Type} (r : Ref σ α) (f : α → α) : m Unit := liftM <| Prim.Ref.modify r f
@[inline] def Ref.modifyGet {α : Type} {β : Type} (r : Ref σ α) (f : α → β × α) : m β := liftM <| Prim.Ref.modifyGet r f
end

4
src/Init/WF.lean
View file

@ -274,7 +274,7 @@ def lexNdep (r : α → α → Prop) (s : β → β → Prop) :=
Lex r (fun a => s)
def lexNdepWf {r : α → α → Prop} {s : β → β → Prop} (ha : WellFounded r) (hb : WellFounded s) : WellFounded (lexNdep r s) :=
WellFounded.intro $ fun ⟨a, b⟩ => lexAccessible (WellFounded.apply ha a) (fun x => hb) b
WellFounded.intro fun ⟨a, b⟩ => lexAccessible (WellFounded.apply ha a) (fun x => hb) b
end
section
@ -304,7 +304,7 @@ def revLexAccessible {b} (acb : Acc s b) (aca : (a : α) → Acc r a): (a : α)
| right => apply ihb; assumption
def revLexWf (ha : WellFounded r) (hb : WellFounded s) : WellFounded (RevLex r s) :=
WellFounded.intro $ fun ⟨a, b⟩ => revLexAccessible (apply hb b) (WellFounded.apply ha) a
WellFounded.intro fun ⟨a, b⟩ => revLexAccessible (apply hb b) (WellFounded.apply ha) a
end
section

6
src/Lean/KeyedDeclsAttribute.lean
View file

@ -91,7 +91,7 @@ private unsafe def addImported {γ} (df : Def γ) (tableRef : IO.Ref (Table γ))
entries.foldlM
(fun (table : Table γ) entry =>
match ctx.env.evalConstCheck γ ctx.opts df.valueTypeName entry.decl with
| Except.ok f => pure $ table.insert entry.key f
| Except.ok f => pure <| table.insert entry.key f
| Except.error ex => throw (IO.userError ex))
table)
table
@ -101,7 +101,7 @@ private def addExtensionEntry {γ} (s : ExtensionState γ) (e : AttributeEntry
{ table := s.table.insert e.key e.value, newEntries := e.toOLeanEntry :: s.newEntries }
def addBuiltin {γ} (attr : KeyedDeclsAttribute γ) (key : Key) (val : γ) : IO Unit :=
attr.tableRef.modify $ fun m => m.insert key val
attr.tableRef.modify fun m => m.insert key val
/--
def _regBuiltin$(declName) : IO Unit :=
@ -154,7 +154,7 @@ protected unsafe def init {γ} (df : Def γ) (attrDeclName : Name) : IO (KeyedDe
let key ← df.evalKey false arg
let val ← evalConstCheck γ df.valueTypeName constName
let env ← getEnv
setEnv $ ext.addEntry env { key := key, decl := constName, value := val },
setEnv <| ext.addEntry env { key := key, decl := constName, value := val },
applicationTime := AttributeApplicationTime.afterCompilation
}
pure { defn := df, tableRef := tableRef, ext := ext }

14
src/Lean/LocalContext.lean
View file

@ -282,13 +282,13 @@ variable {β : Type u}
end
@[inline] def foldl {β} (lctx : LocalContext) (f : β → LocalDecl → β) (init : β) (start : Nat := 0) : β :=
Id.run $ lctx.foldlM f init start
Id.run <| lctx.foldlM f init start
@[inline] def findDecl? {β} (lctx : LocalContext) (f : LocalDecl → Option β) : Option β :=
Id.run $ lctx.findDeclM? f
Id.run <| lctx.findDeclM? f
@[inline] def findDeclRev? {β} (lctx : LocalContext) (f : LocalDecl → Option β) : Option β :=
Id.run $ lctx.findDeclRevM? f
Id.run <| lctx.findDeclRevM? f
partial def isSubPrefixOfAux (a₁ a₂ : PArray (Option LocalDecl)) (exceptFVars : Array Expr) (i j : Nat) : Bool :=
if i < a₁.size then
@ -353,10 +353,10 @@ variables {m : Type → Type u} [Monad m]
end
@[inline] def any (lctx : LocalContext) (p : LocalDecl → Bool) : Bool :=
Id.run $ lctx.anyM p
Id.run <| lctx.anyM p
@[inline] def all (lctx : LocalContext) (p : LocalDecl → Bool) : Bool :=
Id.run $ lctx.allM p
Id.run <| lctx.allM p
def sanitizeNames (lctx : LocalContext) : StateM NameSanitizerState LocalContext := do
let st ← get
@ -368,10 +368,10 @@ def sanitizeNames (lctx : LocalContext) : StateM NameSanitizerState LocalContext
| none => pure lctx
| some decl => do
let usedNames ← get
set $ usedNames.insert decl.userName
set <| usedNames.insert decl.userName
if decl.userName.hasMacroScopes || usedNames.contains decl.userName then do
let userNameNew ← sanitizeName decl.userName
pure $ lctx.setUserName decl.fvarId userNameNew
pure <| lctx.setUserName decl.fvarId userNameNew
else
pure lctx)
lctx

14
src/Lean/Meta/Offset.lean
View file

@ -19,31 +19,31 @@ partial def evalNat : Expr → Option Nat
let nargs := e.getAppNumArgs
if c == `Nat.succ && nargs == 1 then
let v ← evalNat a
pure $ v+1
return v+1
else if c == `Nat.add && nargs == 2 then
let v₁ ← evalNat (e.getArg! 0)
let v₂ ← evalNat (e.getArg! 1)
pure $ v₁ + v₂
return v₁ + v₂
else if c == `Nat.sub && nargs == 2 then
let v₁ ← evalNat (e.getArg! 0)
let v₂ ← evalNat (e.getArg! 1)
pure $ v₁ - v₂
return v₁ - v₂
else if c == `Nat.mul && nargs == 2 then
let v₁ ← evalNat (e.getArg! 0)
let v₂ ← evalNat (e.getArg! 1)
pure $ v₁ * v₂
return v₁ * v₂
else if c == `Add.add && nargs == 4 then
let v₁ ← evalNat (e.getArg! 2)
let v₂ ← evalNat (e.getArg! 3)
pure $ v₁ + v₂
return v₁ + v₂
else if c == `Sub.sub && nargs == 4 then
let v₁ ← evalNat (e.getArg! 2)
let v₂ ← evalNat (e.getArg! 3)
pure $ v₁ - v₂
return v₁ - v₂
else if c == `Mul.mul && nargs == 4 then
let v₁ ← evalNat (e.getArg! 2)
let v₂ ← evalNat (e.getArg! 3)
pure $ v₁ * v₂
return v₁ * v₂
else if c == `OfNat.ofNat && nargs == 3 then
evalNat (e.getArg! 2)
else

4
src/Lean/ParserCompiler/Attribute.lean
View file

@ -32,8 +32,8 @@ def registerCombinatorAttribute (name : Name) (descr : String)
match attrParamSyntaxToIdentifier args with
| some parserDeclName => do
getConstInfo parserDeclName
setEnv $ ext.addEntry env (parserDeclName, decl)
| none => throwError $ "invalid [" ++ name ++ "] argument, expected identifier"
setEnv <| ext.addEntry env (parserDeclName, decl)
| none => throwError! "invalid [{name}] argument, expected identifier"
}
registerBuiltinAttribute attrImpl
pure { impl := attrImpl, ext := ext }

6
src/Lean/Structure.lean
View file

@ -48,7 +48,7 @@ private def getStructureFieldsAux (nparams : Nat) : Nat → Expr → Array Name
if i < nparams then
getStructureFieldsAux nparams (i+1) b fieldNames
else
getStructureFieldsAux nparams (i+1) b (fieldNames.push $ deinternalizeFieldName n)
getStructureFieldsAux nparams (i+1) b <| fieldNames.push <| deinternalizeFieldName n
| _, _, fieldNames => fieldNames
-- TODO: fix. See comment in the beginning of the file
@ -87,7 +87,7 @@ partial def findField? (env : Environment) (structName : Name) (fieldName : Name
if (getStructureFields env structName).contains fieldName then
some structName
else
(getParentStructures env structName).findSome? $ fun parentStructName => findField? env parentStructName fieldName
getParentStructures env structName |>.findSome? fun parentStructName => findField? env parentStructName fieldName
private partial def getStructureFieldsFlattenedAux (env : Environment) (structName : Name) (fullNames : Array Name) : Array Name :=
(getStructureFields env structName).foldl (init := fullNames) fun fullNames fieldName =>
@ -135,7 +135,7 @@ partial def getPathToBaseStructureAux (env : Environment) (baseStructName : Name
some path.reverse
else
let fieldNames := getStructureFields env structName;
fieldNames.findSome? $ fun fieldName =>
fieldNames.findSome? fun fieldName =>
match isSubobjectField? env structName fieldName with
| none => none
| some parentStructName =>

2
src/Lean/Util/FindExpr.lean
View file

@ -49,7 +49,7 @@ unsafe def initCache : State :=
{ keys := mkArray cacheSize.toNat (cast lcProof ()) }
@[inline] unsafe def findUnsafe? (p : Expr → Bool) (e : Expr) : Option Expr :=
Id.run $ (findM? p cacheSize e).run' initCache
Id.run <| findM? p cacheSize e |>.run' initCache
end FindImpl

14
src/Lean/Util/ReplaceExpr.lean
View file

@ -28,16 +28,16 @@ abbrev ReplaceM := StateM State
let h := ptrAddrUnsafe e
let i := h % size
if ptrAddrUnsafe (c.keys.uget i lcProof) == h then
pure $ c.results.uget i lcProof
pure <| c.results.uget i lcProof
else match f? e with
| some eNew => cache i e eNew
| none => match e with
| Expr.forallE _ d b _ => cache i e $ e.updateForallE! (← visit d) (← visit b)
| Expr.lam _ d b _ => cache i e $ e.updateLambdaE! (← visit d) (← visit b)
| Expr.mdata _ b _ => cache i e $ e.updateMData! (← visit b)
| Expr.letE _ t v b _ => cache i e $ e.updateLet! (← visit t) (← visit v) (← visit b)
| Expr.app f a _ => cache i e $ e.updateApp! (← visit f) (← visit a)
| Expr.proj _ _ b _ => cache i e $ e.updateProj! (← visit b)
| Expr.forallE _ d b _ => cache i e <| e.updateForallE! (← visit d) (← visit b)
| Expr.lam _ d b _ => cache i e <| e.updateLambdaE! (← visit d) (← visit b)
| Expr.mdata _ b _ => cache i e <| e.updateMData! (← visit b)
| Expr.letE _ t v b _ => cache i e <| e.updateLet! (← visit t) (← visit v) (← visit b)
| Expr.app f a _ => cache i e <| e.updateApp! (← visit f) (← visit a)
| Expr.proj _ _ b _ => cache i e <| e.updateProj! (← visit b)
| e => pure e
visit e

18
src/Lean/Util/ReplaceLevel.lean
View file

@ -41,16 +41,16 @@ abbrev ReplaceM := StateM State
let h := ptrAddrUnsafe e
let i := h % size
if ptrAddrUnsafe (c.keys.uget i lcProof) == h then
pure $ c.results.uget i lcProof
pure <| c.results.uget i lcProof
else match e with
| Expr.forallE _ d b _ => cache i e $ e.updateForallE! (← visit d) (← visit b)
| Expr.lam _ d b _ => cache i e $ e.updateLambdaE! (← visit d) (← visit b)
| Expr.mdata _ b _ => cache i e $ e.updateMData! (← visit b)
| Expr.letE _ t v b _ => cache i e $ e.updateLet! (← visit t) (← visit v) (← visit b)
| Expr.app f a _ => cache i e $ e.updateApp! (← visit f) (← visit a)
| Expr.proj _ _ b _ => cache i e $ e.updateProj! (← visit b)
| Expr.sort u _ => cache i e $ e.updateSort! (u.replace f?)
| Expr.const n us _ => cache i e $ e.updateConst! (us.map (Level.replace f?))
| Expr.forallE _ d b _ => cache i e <| e.updateForallE! (← visit d) (← visit b)
| Expr.lam _ d b _ => cache i e <| e.updateLambdaE! (← visit d) (← visit b)
| Expr.mdata _ b _ => cache i e <| e.updateMData! (← visit b)
| Expr.letE _ t v b _ => cache i e <| e.updateLet! (← visit t) (← visit v) (← visit b)
| Expr.app f a _ => cache i e <| e.updateApp! (← visit f) (← visit a)
| Expr.proj _ _ b _ => cache i e <| e.updateProj! (← visit b)
| Expr.sort u _ => cache i e <| e.updateSort! (u.replace f?)
| Expr.const n us _ => cache i e <| e.updateConst! (us.map (Level.replace f?))
| e => pure e
visit e