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_monadLift {α ε : Type u} {m : Type u → Type v} {n : Type u → Type u_1} [Monad m] [MonadLiftT n m] (x : n α) :
    @[simp]
    theorem ExceptT.run_monadMap {α ε : Type u} {m : Type u → Type v} (x : ExceptT ε m α) {n : Type u → Type u_1} [MonadFunctorT n m] (f : {α : Type u} → n αn α) :
    def ReaderT.mk {m : Type u → Type v} {α σ : Type u} (f : σm α) :
    ReaderT σ m α
    Equations
    Instances For
      @[simp]
      theorem ReaderT.run_mk {m : Type u → Type v} {α σ : Type u} (f : σm α) (r : σ) :
      (ReaderT.mk f).run r = f r