Documentation

Mathlib.Control.Monad.Basic

Monad #

Attributes #

Implementation Details #

Set of rewrite rules and automation for monads in general and ReaderT, StateT, ExceptT and OptionT in particular.

The rewrite rules for monads are carefully chosen so that simp with functor_norm will not introduce monadic vocabulary in a context where applicatives would do just fine but will handle monadic notation already present in an expression.

In a context where monadic reasoning is desired simp with monad_norm will translate functor and applicative notation into monad notation and use regular functor_norm rules as well.

Tags #

functor, applicative, monad, simp

theorem ReaderT.ext_iff {ρ : Type u_1} {m : Type u_1 → Type u_2} {α : Type u_1} {x : ReaderT ρ m α} {y : ReaderT ρ m α} :
x = y ∀ (ctx : ρ), x.run ctx = y.run ctx
theorem ExceptT.ext_iff {ε : Type u_1} {m : Type u_1 → Type u_2} {α : Type u_1} {x : ExceptT ε m α} {y : ExceptT ε m α} :
x = y x.run = y.run
theorem StateT.ext_iff {σ : Type u_1} {m : Type u_1 → Type u_2} {α : Type u_1} {x : StateT σ m α} {y : StateT σ m α} :
x = y ∀ (s : σ), x.run s = y.run s
theorem map_eq_bind_pure_comp {α : Type u} {β : Type u} (m : Type u → Type v) [Monad m] [LawfulMonad m] (f : αβ) (x : m α) :
f <$> x = x >>= pure f
def StateT.eval {α : Type u} {σ : Type u} {m : Type u → Type v} [Functor m] (cmd : StateT σ m α) (s : σ) :
m α

run a StateT program and discard the final state

Equations
  • cmd.eval s = Prod.fst <$> cmd.run s
Instances For
    def StateT.equiv {σ₁ : Type u₀} {α₁ : Type u₀} {σ₂ : Type u₁} {α₂ : Type u₁} {m₁ : Type u₀ → Type v₀} {m₂ : Type u₁ → Type v₁} (F : (σ₁m₁ (α₁ × σ₁)) (σ₂m₂ (α₂ × σ₂))) :
    StateT σ₁ m₁ α₁ StateT σ₂ m₂ α₂

    reduce the equivalence between two state monads to the equivalence between their respective function spaces

    Equations
    Instances For
      def ReaderT.equiv {ρ₁ : Type u₀} {α₁ : Type u₀} {ρ₂ : Type u₁} {α₂ : Type u₁} {m₁ : Type u₀ → Type v₀} {m₂ : Type u₁ → Type v₁} (F : (ρ₁m₁ α₁) (ρ₂m₂ α₂)) :
      ReaderT ρ₁ m₁ α₁ ReaderT ρ₂ m₂ α₂

      reduce the equivalence between two reader monads to the equivalence between their respective function spaces

      Equations
      Instances For