mathlib documentation

control.monad.basic

Monad #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. https://github.com/leanprover-community/mathlib4/pull/752 Any changes to this file require a corresponding PR to mathlib4.

Attributes #

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 u Type v) [monad m] [is_lawful_monad m] {α β : Type u} (f : α β) (x : m α) :
def state_t.eval {m : Type u Type v} [functor m] {σ α : Type u} (cmd : state_t σ 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