mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
27b583d304
This PR changes the elaboration of the `structure`/`class` commands so that default values have later fields in context as well. This allows field defaults to depend on fields that come both before and after them. While this was already the case for inherited fields to some degree, it now applies uniformly to all fields. Additionally, when elaborating the default value for a field, all fields that depend on it are cleared from the context to avoid situations where the default value depends on itself. This addresses an issue reported by Aaron Liu [on Zulip](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/default.20structure.20values.20can.20depend.20on.20themselves/near/578014370).
36 lines
1.7 KiB
Lean4
36 lines
1.7 KiB
Lean4
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 ()
|
||
|
||
/-!
|
||
Can provide type signatures when setting defaults of inherited fields.
|
||
-/
|
||
class Monad5 (m : Type u → Type v) : Type (max (u+1) v) extends Applicative m, Bind2 m where
|
||
map {α β} (f : α → β) (x : m α) : m β :=
|
||
Bind2.bind x (pure ∘ f)
|
||
seq {α β} (f : m (α → β)) (x : Unit -> m α) : m β :=
|
||
Bind2.bind f fun y => Functor.map y (x ())
|
||
seqLeft {α β} (x : m α) (y : Unit → m β) :=
|
||
Bind2.bind x fun a => Bind2.bind (y ()) fun _ => pure a
|
||
seqRight {α β} (x : m α) (y : Unit → m β) :=
|
||
Bind2.bind x fun _ => y ()
|