Mathlib.Init.Control.Lawful

Functor Laws, applicative laws, and monad Laws #

source

def StateT.mk {σ : Type u} {m : Type u → Type v} {α : Type u} (f : σ → m (α × σ)) :

StateT σ m α

Equations

StateT.mk f = f

Instances For

source

@[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

source

@[simp]

theorem ExceptT.run_mk {α : Type u} {ε : Type u} {m : Type u → Type v} (x : m (Except ε α)) :

ExceptT.run (ExceptT.mk x) = x

source

@[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

source

@[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)

source

def ReaderT.mk {m : Type u → Type v} {α : Type u} {σ : Type u} (f : σ → m α) :

ReaderT σ m α

Equations

ReaderT.mk f = f

Instances For

source

@[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

source

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'

source

@[simp]

theorem OptionT.run_mk {α : Type u} {m : Type u → Type v} (x : m (Option α)) :

OptionT.run (OptionT.mk x) = x

source

@[simp]

theorem OptionT.run_pure {α : Type u} {m : Type u → Type v} [Monad m] (a : α) :

OptionT.run (pure a) = pure (some a)

source

@[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

source

@[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

source

@[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 α) :

OptionT.run (monadLift x) = do let a ← monadLift x pure (some a)

source

@[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)

source

instance instLawfulMonadOptionTInstMonadOptionT (m : Type u → Type v) [Monad m] [LawfulMonad m] :

LawfulMonad (OptionT m)

Equations

(_ : LawfulMonad (OptionT m)) = (_ : LawfulMonad (OptionT m))

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.

source

instance instLawfulMonadEIOInstMonadEIO {ε : Type} :

LawfulMonad (EIO ε)

Equations