# mathlibdocumentation

• ext
• functor_norm

## Implementation Details #

Set of rewrite rules and automation for monads in general and reader_t, state_t, except_t and option_t 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

simp set for monad_norm

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

run a state_t program and discard the final state

Equations
def state_t.equiv {m₁ : Type u₀Type v₀} {m₂ : Type u₁Type v₁} {α₁ σ₁ : Type u₀} {α₂ σ₂ : Type u₁} (F : (σ₁ → m₁ (α₁ × σ₁)) (σ₂ → m₂ (α₂ × σ₂))) :
state_t σ₁ m₁ α₁ state_t σ₂ m₂ α₂

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

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

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

Equations