Documentation

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