finish equation syntax change

library/init/control/alternative.lean

@@ -29,8 +29,8 @@ if h : p then pure ⟨h⟩ else failure
 /- Later we define a coercion from Bool to Prop, but this version will still be useful.
    Given (t : tactic Bool), we can write t >>= guardb -/
 @[inline] def guardb {f : Type → Type v} [Alternative f] : Bool → f Unit
-| true  := pure ()
-| false := failure
+| true  => pure ()
+| false => failure
 
 @[inline] def optional (x : f α) : f (Option α) :=
 some <$> x <|> pure none

library/init/control/combinators.lean

@@ -33,15 +33,15 @@ mcond c t (pure ())
 namespace Nat
 
 @[specialize] def mforAux {m} [Applicative m] (f : Nat → m Unit) (n : Nat) : Nat → m Unit
-| 0     := pure ()
-| (i+1) := f (n-i-1) *> mforAux i
+| 0     => pure ()
+| i+1   => f (n-i-1) *> mforAux i
 
 @[inline] def mfor {m} [Applicative m] (n : Nat) (f : Nat → m Unit) : m Unit :=
 mforAux f n n
 
 @[specialize] def mfoldAux {α : Type u} {m : Type u → Type v} [Monad m] (f : Nat → α → m α) (n : Nat) : Nat → α → m α
-| 0     a := pure a
-| (i+1) a := f (n-i-1) a >>= mfoldAux i
+| 0,     a => pure a
+| i+1,   a => f (n-i-1) a >>= mfoldAux i
 
 @[inline] def mfold {α : Type u} {m : Type u → Type v} [Monad m] (f : Nat → α → m α) (a : α) (n : Nat) : m α :=
 mfoldAux f n n a
@@ -59,49 +59,49 @@ namespace List
 
 @[specialize]
 def mmap {m : Type u → Type v} [Applicative m] {α : Type w} {β : Type u} (f : α → m β) : List α → m (List β)
-| []      := pure []
-| (a::as) := List.cons <$> (f a) <*> mmap as
+| []      => pure []
+| a::as   => List.cons <$> (f a) <*> mmap as
 
 @[specialize]
 def mfor {m : Type u → Type v} [Applicative m] {α : Type w} {β : Type u} (f : α → m β) : List α → m PUnit
-| []       := pure ⟨⟩
-| (h :: t) := f h *> mfor t
+| []       => pure ⟨⟩
+| h :: t   => f h *> mfor t
 
 @[specialize]
 def mfilter {m : Type → Type v} [Monad m] {α : Type} (f : α → m Bool) : List α → m (List α)
-| []       := pure []
-| (h :: t) := do b ← f h; t' ← mfilter t; cond b (pure (h :: t')) (pure t')
+| []       => pure []
+| h :: t   => do b ← f h; t' ← mfilter t; cond b (pure (h :: t')) (pure t')
 
 @[specialize]
 def mfoldl {m : Type u → Type v} [Monad m] {s : Type u} {α : Type w} : (s → α → m s) → s → List α → m s
-| f s [] := pure s
-| f s (h :: r) := do
+| f, s, [] => pure s
+| f, s, h :: r   => do
   s' ← f s h;
   mfoldl f s' r
 
 @[specialize]
 def mfoldr {m : Type u → Type v} [Monad m] {s : Type u} {α : Type w} : (α → s → m s) → s → List α → m s
-| f s [] := pure s
-| f s (h :: r) := do
+| f, s, [] => pure s
+| f, s, h :: r   => do
   s' ← mfoldr f s r;
   f h s'
 
 @[specialize]
 def mfirst {m : Type u → Type v} [Monad m] [Alternative m] {α : Type w} {β : Type u} (f : α → m β) : List α → m β
-| []      := failure
-| (a::as) := f a <|> mfirst as
+| []      => failure
+| a::as   => f a <|> mfirst as
 
 @[specialize]
 def mexists {m : Type → Type u} [Monad m] {α : Type v} (f : α → m Bool) : List α → m Bool
-| []      := pure false
-| (a::as) := do b ← f a; match b with
+| []      => pure false
+| a::as   => do b ← f a; match b with
   | true  => pure true
   | false =>  mexists as
 
 @[specialize]
 def mforall {m : Type → Type u} [Monad m] {α : Type v} (f : α → m Bool) : List α → m Bool
-| []      := pure true
-| (a::as) := do b ← f a; match b with
+| []      => pure true
+| a::as   => do b ← f a; match b with
   | true  => mforall as
   | false => pure false
 

library/init/control/estate.lean

@@ -34,12 +34,12 @@ abbrev resultOk (ε σ α : Type u) := {r : Result ε σ α // r.IsOk}
 ⟨Result.ok a s, Result.IsOk.mk a s⟩
 
 protected def Result.toString [HasToString ε] [HasToString α] : Result ε σ α → String
-| (Result.ok a _)    := "ok: " ++ toString a
-| (Result.error e _) := "error: " ++ toString e
+| Result.ok a _      => "ok: " ++ toString a
+| Result.error e _   => "error: " ++ toString e
 
 protected def Result.repr [HasRepr ε] [HasRepr α] : Result ε σ α → String
-| (Result.error e _) := "(error " ++ repr e ++ ")"
-| (Result.ok a _)    := "(ok " ++ repr a ++ ")"
+| Result.error e _   => "(error " ++ repr e ++ ")"
+| Result.ok a _      => "(ok " ++ repr a ++ ")"
 
 instance [HasToString ε] [HasToString α] : HasToString (Result ε σ α) := ⟨Result.toString⟩
 instance [HasRepr ε] [HasRepr α] : HasRepr (Result ε σ α) := ⟨Result.repr⟩

library/init/control/except.lean

@@ -21,12 +21,12 @@ section
 variables {ε : Type u} {α : Type v}
 
 protected def Except.toString [HasToString ε] [HasToString α] : Except ε α → String
-| (Except.error e) := "(error " ++ toString e ++ ")"
-| (Except.ok a)    := "(ok " ++ toString a ++ ")"
+| Except.error e   => "(error " ++ toString e ++ ")"
+| Except.ok a      => "(ok " ++ toString a ++ ")"
 
 protected def Except.repr [HasRepr ε] [HasRepr α] : Except ε α → String
-| (Except.error e) := "(error " ++ repr e ++ ")"
-| (Except.ok a)    := "(ok " ++ repr a ++ ")"
+| Except.error e   => "(error " ++ repr e ++ ")"
+| Except.ok a      => "(ok " ++ repr a ++ ")"
 
 instance [HasToString ε] [HasToString α] : HasToString (Except ε α) :=
 ⟨Except.toString⟩
@@ -42,25 +42,25 @@ variables {ε : Type u}
 Except.ok a
 
 @[inline] protected def map {α β : Type v} (f : α → β) : Except ε α → Except ε β
-| (Except.error err) := Except.error err
-| (Except.ok v) := Except.ok $ f v
+| Except.error err   => Except.error err
+| 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.ok v) := Except.ok v
+| Except.error err   => Except.error $ f err
+| Except.ok v   => Except.ok v
 
 @[inline] protected def bind {α β : Type v} (ma : Except ε α) (f : α → Except ε β) : Except ε β :=
 match ma with
 | (Except.error err) => Except.error err
 | (Except.ok v)      => f v
 
 @[inline] protected def toBool {α : Type v} : Except ε α → Bool
-| (Except.ok _)    := true
-| (Except.error _) := false
+| Except.ok _      => true
+| Except.error _   => false
 
 @[inline] protected def toOption {α : Type v} : Except ε α → Option α
-| (Except.ok a)    := some a
-| (Except.error _) := none
+| Except.ok a      => some a
+| Except.error _   => none
 
 @[inline] protected def catch {α : Type u} (ma : Except ε α) (handle : ε → Except ε α) : Except ε α :=
 match ma with
@@ -87,8 +87,8 @@ variables {ε : Type u} {m : Type u → Type v} [Monad m]
 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)
+| 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
@@ -139,8 +139,8 @@ catch t₁ $ fun _ => t₂
 catch t₁ $ fun e₁ => catch t₂ $ fun e₂ => throw (if useFirstEx then e₁ else e₂)
 
 @[inline] def liftExcept {ε' : Type u} [MonadExcept ε m] [HasLiftT ε' ε] [Monad m] {α : Type v} : Except ε' α → m α
-| (Except.error e) := throw (coe e)
-| (Except.ok a)    := pure a
+| Except.error e   => throw (coe e)
+| Except.ok a      => pure a
 end MonadExcept
 
 export MonadExcept (throw catch)

library/init/control/option.lean

@@ -18,8 +18,8 @@ namespace OptionT
   variables {m : Type u → Type v} [Monad m] {α β : Type u}
 
   @[inline] protected def bindCont {α β : Type u} (f : α → OptionT m β) : Option α → m (Option β)
-  | (some a) := f a
-  | none     := pure none
+  | some a   => f a
+  | none     => pure none
 
   @[inline] protected def bind (ma : OptionT m α) (f : α → OptionT m β) : OptionT m β :=
   (ma >>= OptionT.bindCont f : m (Option β))