# Documentation

• ext
• functor_norm

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

theorem map_eq_bind_pure_comp {α : Type u} {β : Type u} (m : Type u → Type v) [inst : ] [inst : ] (f : αβ) (x : m α) :
f <\$> x = x >>= pure f
def StateT.eval {σ : Type u} {α : Type u} {m : Type u → Type v} [inst : ] (cmd : StateT σ m α) (s : σ) :
m α

run a StateT program and discard the final state

Equations
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
def ReaderT.equiv {ρ₁ : Type u₀} {α₁ : Type u₀} {ρ₂ : Type u₁} {α₂ : Type u₁} {m₁ : Type u₀ → Type v₀} {m₂ : Type u₁ → Type v₁} (F : (ρ₁m₁ α₁) (ρ₂m₂ α₂)) :