mathlib3 documentation

control.monad.basic

Monad #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. 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

source
theorem map_eq_bind_pure_comp (m : Type u → Type v) [monad m] [is_lawful_monad m] {α β : Type u} (f : α → β) (x : m α) :
f <$> x = x >>= has_pure.pure ∘ f
source
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
source
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
source
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