From 304c80d6108eb2e8ff6c554bd8befb932506805e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 19 Nov 2020 09:03:38 -0800 Subject: [PATCH] feat: use `<|` --- src/Init/Classical.lean | 4 +-- src/Init/Coe.lean | 2 +- src/Init/Control/Except.lean | 30 +++++++++--------- src/Init/Core.lean | 6 ++-- src/Init/Data/Array/Basic.lean | 38 +++++++++++------------ src/Init/Data/Array/BinSearch.lean | 16 +++++----- src/Init/Data/Array/Subarray.lean | 8 ++--- src/Init/Data/Int/Basic.lean | 18 +++++------ src/Init/Data/Nat/Basic.lean | 2 +- src/Init/Data/Repr.lean | 6 ++-- src/Init/Data/String/Basic.lean | 12 +++---- src/Init/Meta.lean | 37 +++++++++++----------- src/Init/System/IO.lean | 43 ++++++++++++++------------ src/Init/System/ST.lean | 20 ++++++------ src/Init/WF.lean | 4 +-- src/Lean/KeyedDeclsAttribute.lean | 6 ++-- src/Lean/LocalContext.lean | 14 ++++----- src/Lean/Meta/Offset.lean | 14 ++++----- src/Lean/ParserCompiler/Attribute.lean | 4 +-- src/Lean/Structure.lean | 6 ++-- src/Lean/Util/FindExpr.lean | 2 +- src/Lean/Util/ReplaceExpr.lean | 14 ++++----- src/Lean/Util/ReplaceLevel.lean | 18 +++++------ 23 files changed, 164 insertions(+), 160 deletions(-) diff --git a/src/Init/Classical.lean b/src/Init/Classical.lean index e658a639d0..ae3801a2b0 100644 --- a/src/Init/Classical.lean +++ b/src/Init/Classical.lean @@ -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⟩ diff --git a/src/Init/Coe.lean b/src/Init/Coe.lean index 3adc4a8307..734d611264 100644 --- a/src/Init/Coe.lean +++ b/src/Init/Coe.lean @@ -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 diff --git a/src/Init/Control/Except.lean b/src/Init/Control/Except.lean index 8a7a5f8431..4e6febb5bb 100644 --- a/src/Init/Control/Except.lean +++ b/src/Init/Control/Except.lean @@ -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 } diff --git a/src/Init/Core.lean b/src/Init/Core.lean index 7deff2ba1c..3fdcbed018 100644 --- a/src/Init/Core.lean +++ b/src/Init/Core.lean @@ -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) diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index 51925584dc..aef9e2eb86 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/src/Init/Data/Array/Basic.lean @@ -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 diff --git a/src/Init/Data/Array/BinSearch.lean b/src/Init/Data/Array/BinSearch.lean index 5172a282f7..63fb792440 100644 --- a/src/Init/Data/Array/BinSearch.lean +++ b/src/Init/Data/Array/BinSearch.lean @@ -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 diff --git a/src/Init/Data/Array/Subarray.lean b/src/Init/Data/Array/Subarray.lean index b71a228eb4..f1af76e1d4 100644 --- a/src/Init/Data/Array/Subarray.lean +++ b/src/Init/Data/Array/Subarray.lean @@ -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 diff --git a/src/Init/Data/Int/Basic.lean b/src/Init/Data/Int/Basic.lean index 6f87d8e529..5e8081cbc8 100644 --- a/src/Init/Data/Int/Basic.lean +++ b/src/Init/Data/Int/Basic.lean @@ -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? diff --git a/src/Init/Data/Nat/Basic.lean b/src/Init/Data/Nat/Basic.lean index 71f3f4fdff..5ddf01a653 100644 --- a/src/Init/Data/Nat/Basic.lean +++ b/src/Init/Data/Nat/Basic.lean @@ -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] diff --git a/src/Init/Data/Repr.lean b/src/Init/Data/Repr.lean index c7f4d7665f..443c9594e6 100644 --- a/src/Init/Data/Repr.lean +++ b/src/Init/Data/Repr.lean @@ -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; diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean index c60d02de92..593c910d06 100644 --- a/src/Init/Data/String/Basic.lean +++ b/src/Init/Data/String/Basic.lean @@ -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 diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean index df6d5fe1dd..c1a60b0723 100644 --- a/src/Init/Meta.lean +++ b/src/Init/Meta.lean @@ -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 diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean index 943916788a..0666feb676 100644 --- a/src/Init/System/IO.lean +++ b/src/Init/System/IO.lean @@ -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 diff --git a/src/Init/System/ST.lean b/src/Init/System/ST.lean index 4ee82168f7..7db8f00502 100644 --- a/src/Init/System/ST.lean +++ b/src/Init/System/ST.lean @@ -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 diff --git a/src/Init/WF.lean b/src/Init/WF.lean index 3e7dc1d747..8fd7a49c9d 100644 --- a/src/Init/WF.lean +++ b/src/Init/WF.lean @@ -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 diff --git a/src/Lean/KeyedDeclsAttribute.lean b/src/Lean/KeyedDeclsAttribute.lean index 7f91e8de10..243a60a012 100644 --- a/src/Lean/KeyedDeclsAttribute.lean +++ b/src/Lean/KeyedDeclsAttribute.lean @@ -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 } diff --git a/src/Lean/LocalContext.lean b/src/Lean/LocalContext.lean index 34ecce6aff..1c3a251b2a 100644 --- a/src/Lean/LocalContext.lean +++ b/src/Lean/LocalContext.lean @@ -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 diff --git a/src/Lean/Meta/Offset.lean b/src/Lean/Meta/Offset.lean index a18348857d..47535f39f2 100644 --- a/src/Lean/Meta/Offset.lean +++ b/src/Lean/Meta/Offset.lean @@ -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 diff --git a/src/Lean/ParserCompiler/Attribute.lean b/src/Lean/ParserCompiler/Attribute.lean index d9c05073ed..3e279dfe0c 100644 --- a/src/Lean/ParserCompiler/Attribute.lean +++ b/src/Lean/ParserCompiler/Attribute.lean @@ -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 } diff --git a/src/Lean/Structure.lean b/src/Lean/Structure.lean index afb5be19f3..3bae2f87d9 100644 --- a/src/Lean/Structure.lean +++ b/src/Lean/Structure.lean @@ -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 => diff --git a/src/Lean/Util/FindExpr.lean b/src/Lean/Util/FindExpr.lean index d7b153b0a9..a060aa46ec 100644 --- a/src/Lean/Util/FindExpr.lean +++ b/src/Lean/Util/FindExpr.lean @@ -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 diff --git a/src/Lean/Util/ReplaceExpr.lean b/src/Lean/Util/ReplaceExpr.lean index d349e86dc5..bc96da2ddd 100644 --- a/src/Lean/Util/ReplaceExpr.lean +++ b/src/Lean/Util/ReplaceExpr.lean @@ -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 diff --git a/src/Lean/Util/ReplaceLevel.lean b/src/Lean/Util/ReplaceLevel.lean index 95987e4051..ba03c82962 100644 --- a/src/Lean/Util/ReplaceLevel.lean +++ b/src/Lean/Util/ReplaceLevel.lean @@ -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