Functor Laws, applicative laws, and monad Laws #
@[simp]
theorem
StateT.run_mk
{σ : Type u}
{m : Type u → Type v}
{α : Type u}
(f : σ → m (α × σ))
(st : σ)
:
StateT.run (StateT.mk f) st = f st
@[simp]
theorem
ExceptT.run_mk
{α : Type u}
{ε : Type u}
{m : Type u → Type v}
(x : m (Except ε α))
:
ExceptT.run (ExceptT.mk x) = x
@[simp]
theorem
ExceptT.run_monadLift
{α : Type u}
{ε : Type u}
{m : Type u → Type v}
[Monad m]
{n : Type u → Type u_1}
[MonadLiftT n m]
(x : n α)
:
ExceptT.run (monadLift x) = Except.ok <$> monadLift x
@[simp]
theorem
ExceptT.run_monadMap
{α : Type u}
{ε : Type u}
{m : Type u → Type v}
(x : ExceptT ε m α)
{n : Type u → Type u_1}
[MonadFunctorT n m]
(f : {α : Type u} → n α → n α)
:
ExceptT.run (monadMap f x) = monadMap f (ExceptT.run x)
Equations
- ReaderT.mk f = f
Instances For
@[simp]
theorem
ReaderT.run_mk
{m : Type u → Type v}
{α : Type u}
{σ : Type u}
(f : σ → m α)
(r : σ)
:
ReaderT.run (ReaderT.mk f) r = f r
theorem
OptionT.ext
{α : Type u}
{m : Type u → Type v}
{x : OptionT m α}
{x' : OptionT m α}
(h : OptionT.run x = OptionT.run x')
:
x = x'
@[simp]
theorem
OptionT.run_mk
{α : Type u}
{m : Type u → Type v}
(x : m (Option α))
:
OptionT.run (OptionT.mk x) = x
@[simp]
theorem
OptionT.run_bind
{α : Type u}
{β : Type u}
{m : Type u → Type v}
(x : OptionT m α)
[Monad m]
(f : α → OptionT m β)
:
OptionT.run (x >>= f) = do
let x ← OptionT.run x
match x with
| some a => OptionT.run (f a)
| none => pure none
@[simp]
theorem
OptionT.run_map
{α : Type u}
{β : Type u}
{m : Type u → Type v}
(x : OptionT m α)
[Monad m]
(f : α → β)
[LawfulMonad m]
:
OptionT.run (f <$> x) = Option.map f <$> OptionT.run x
@[simp]
theorem
OptionT.run_monadLift
{α : Type u}
{m : Type u → Type v}
[Monad m]
{n : Type u → Type u_1}
[MonadLiftT n m]
(x : n α)
:
@[simp]
theorem
OptionT.run_monadMap
{α : Type u}
{m : Type u → Type v}
(x : OptionT m α)
{n : Type u → Type u_1}
[MonadFunctorT n m]
(f : {α : Type u} → n α → n α)
:
OptionT.run (monadMap f x) = monadMap f (OptionT.run x)
instance
instLawfulMonadOptionTInstMonadOptionT
(m : Type u → Type v)
[Monad m]
[LawfulMonad m]
:
LawfulMonad (OptionT m)
Equations
- ⋯ = ⋯
Lawfulness of IO #
At some point core intends to make IO opaque, which would break these proofs
As discussed in https://github.com/leanprover/std4/pull/416,
it should be possible for core to expose the lawfulness of IO as part of the opaque interface,
which would remove the need for these proofs anyway.
These are not in Std because Std does not want to deal with the churn from such a core refactor.
Equations
Equations
Equations
- ⋯ = ⋯