7557542bc2
This PR modifies the `structure` syntax so that parents can be named, like in ```lean structure S extends toParent : P ``` **Breaking change:** The syntax is also modified so that the resultant type comes *before* the `extends` clause, for example `structure S : Prop extends P`. This is necessary to prevent a parsing ambiguity, but also this is the natural place for the resultant type. Implements RFC #7099. Will need followup PRs for cleanup after a stage0 update.
22 lines
1.1 KiB
Text
22 lines
1.1 KiB
Text
universe u v
|
||
|
||
class Bind2 (m : Type u → Type v) where
|
||
bind : ∀ {α β : Type u}, m α → (α → m β) → m β
|
||
|
||
class Monad2 (m : Type u → Type v) : Type (max (u+1) v) extends Applicative m, Bind2 m where
|
||
map := fun f x => Bind2.bind x (pure ∘ f)
|
||
seq := fun f x => Bind2.bind f fun y => Functor.map y (x ())
|
||
seqLeft := fun x y => Bind2.bind x fun a => Bind2.bind (y ()) fun _ => pure a
|
||
seqRight := @fun α β x y => Bind2.bind x fun _ => y () -- Recall that `@` disables implicit lambda support
|
||
|
||
class Monad3 (m : Type u → Type v) : Type (max (u+1) v) extends Applicative m, Bind2 m where
|
||
map (f x) := Bind2.bind x (pure ∘ f)
|
||
seq (f x) := Bind2.bind f fun y => Functor.map y (x ())
|
||
seqLeft (x y) := Bind2.bind x fun a => Bind2.bind (y ()) fun _ => pure a
|
||
seqRight (x y) := Bind2.bind x fun _ => y ()
|
||
|
||
class Monad4 (m : Type u → Type v) : Type (max (u+1) v) extends Applicative m, Bind2 m where
|
||
map f x := Bind2.bind x (pure ∘ f)
|
||
seq f x := Bind2.bind f fun y => Functor.map y (x ())
|
||
seqLeft x y := Bind2.bind x fun a => Bind2.bind (y ()) fun _ => pure a
|
||
seqRight x y := Bind2.bind x fun _ => y ()
|