Documentation

Mathlib.Control.Lawful

Functor Laws, applicative laws, and monad Laws #

def StateT.mk {σ : Type u} {m : Type u → Type v} {α : Type u} (f : σm (α × σ)) :
StateT σ m α
Equations
Instances For
    @[simp]
    theorem StateT.run_mk {σ : Type u} {m : Type u → Type v} {α : Type u} (f : σm (α × σ)) (st : σ) :
    (StateT.mk f).run st = f st
    @[simp]
    theorem ExceptT.run_mk {α : Type u} {ε : Type u} {m : Type u → Type v} (x : m (Except ε α)) :
    (ExceptT.mk x).run = x
    @[simp]
    theorem ExceptT.run_monadLift {α : Type u} {ε : Type u} {m : Type u → Type v} {n : Type u → Type u_1} [Monad m] [MonadLiftT n m] (x : n α) :
    (monadLift x).run = 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 α) :
    (monadMap f x).run = monadMap f x.run
    def ReaderT.mk {m : Type u → Type v} {α : Type u} {σ : Type u} (f : σm α) :
    ReaderT σ m α
    Equations
    Instances For
      @[simp]
      theorem ReaderT.run_mk {m : Type u → Type v} {α : Type u} {σ : Type u} (f : σm α) (r : σ) :
      (ReaderT.mk f).run r = f r
      theorem OptionT.ext_iff {α : Type u} {m : Type u → Type v} {x : OptionT m α} {x' : OptionT m α} :
      x = x' x.run = x'.run
      theorem OptionT.ext {α : Type u} {m : Type u → Type v} {x : OptionT m α} {x' : OptionT m α} (h : x.run = x'.run) :
      x = x'
      @[simp]
      theorem OptionT.run_mk {α : Type u} {m : Type u → Type v} (x : m (Option α)) :
      (OptionT.mk x).run = x
      @[simp]
      theorem OptionT.run_pure {α : Type u} {m : Type u → Type v} [Monad m] (a : α) :
      (pure a).run = pure (some a)
      @[simp]
      theorem OptionT.run_bind {α : Type u} {β : Type u} {m : Type u → Type v} (x : OptionT m α) [Monad m] (f : αOptionT m β) :
      (x >>= f).run = do let xx.run match x with | some a => (f a).run | 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] :
      (f <$> x).run = Option.map f <$> x.run
      @[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 α) :
      (monadLift x).run = do let amonadLift x pure (some a)
      @[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 α) :
      (monadMap f x).run = monadMap f x.run
      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 Batteries because Batteries does not want to deal with the churn from such a core refactor.

      Equations
      • =
      instance instLawfulMonadEST_mathlib {ε : Type} {σ : Type} :
      Equations
      • =
      Equations
      • =