# 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

theorem map_eq_bind_pure_comp (m : Type uType v) [monad m] {α β : Type u} (f : α → β) (x : m α) :
f <\$> x = x >>=

def state_t.eval {m : Type uType v} [functor m] {σ α : Type u} :
m ασ → 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₁} :
(σ₁ → 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₁} :
(ρ₁ → m₁ α₁) (ρ₂ → m₂ α₂)reader_t ρ₁ m₁ α₁ reader_t ρ₂ m₂ α₂

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

Equations