mathlib documentation

core.init.control.reader

structure reader_t  :
Type u(Type uType v)Type uType (max u v)
  • run : ρ → m α

An implementation of ReaderT

def reader  :
Type uType uType u

Equations
def reader_t.read {ρ : Type u} {m : Type uType v} [monad m] :
reader_t ρ m ρ

Equations
def reader_t.pure {ρ : Type u} {m : Type uType v} [monad m] {α : Type u} :
α → reader_t ρ m α

Equations
def reader_t.bind {ρ : Type u} {m : Type uType v} [monad m] {α β : Type u} :
reader_t ρ m α(α → reader_t ρ m β)reader_t ρ m β

Equations
@[instance]
def reader_t.monad {ρ : Type u} {m : Type uType v} [monad m] :

Equations
def reader_t.lift {ρ : Type u} {m : Type uType v} [monad m] {α : Type u} :
m αreader_t ρ m α

Equations
@[instance]
def reader_t.has_monad_lift {ρ : Type u} (m : Type uType u_1) [monad m] :

Equations
def reader_t.monad_map {ρ : Type u_1} {m : Type u_1Type u_2} {m' : Type u_1Type u_3} [monad m] [monad m'] {α : Type u_1} :
(Π {α : Type u_1}, m αm' α)reader_t ρ m αreader_t ρ m' α

Equations
@[instance]
def reader_t.monad_functor (ρ : Type u_1) (m m' : Type u_1Type u_2) [monad m] [monad m'] :
monad_functor m m' (reader_t ρ m) (reader_t ρ m')

Equations
def reader_t.adapt {ρ : Type u} {m : Type uType v} [monad m] {ρ' : Type u} [monad m] {α : Type u} :
(ρ' → ρ)reader_t ρ m αreader_t ρ' m α

Equations
def reader_t.orelse {ρ : Type u} {m : Type uType v} [monad m] [alternative m] {α : Type u} :
reader_t ρ m αreader_t ρ m αreader_t ρ m α

Equations
def reader_t.failure {ρ : Type u} {m : Type uType v} [monad m] [alternative m] {α : Type u} :
reader_t ρ m α

Equations
@[instance]
def reader_t.alternative {ρ : Type u} {m : Type uType v} [monad m] [alternative m] :

Equations
@[instance]
def reader_t.monad_except {ρ : Type u} {m : Type uType v} [monad m] (ε : out_param (Type u_1)) [monad m] [monad_except ε m] :

Equations
@[class]
structure monad_reader  :
out_param (Type u)(Type uType v)Type v
  • read : m ρ

An implementation of MonadReader. It does not contain local because this function cannot be lifted using monad_lift. Instead, the monad_reader_adapter class provides the more general adapt_reader function.

Note: This class can be seen as a simplification of the more "principled" definition lean class monad_reader (ρ : out_param (Type u)) (n : Type u → Type u) := (lift {α : Type u} : (∀ {m : Type u → Type u} [monad m], reader_t ρ m α) → n α)

Instances
@[instance]
def monad_reader_trans {ρ : Type u} {m : Type uType v} {n : Type uType w} [monad_reader ρ m] [has_monad_lift m n] :

Equations
@[instance]
def reader_t.monad_reader {ρ : Type u} {m : Type uType v} [monad m] :

Equations
@[class]
structure monad_reader_adapter  :
out_param (Type u)out_param (Type u)(Type uType v)(Type uType v)Type (max (u+1) v)
  • adapt_reader : Π {α : Type ?}, (ρ' → ρ)m αm' α

Adapt a monad stack, changing the type of its top-most environment.

This class is comparable to Control.Lens.Magnify, but does not use lenses (why would it), and is derived automatically for any transformer implementing monad_functor.

Note: This class can be seen as a simplification of the more "principled" definition lean class monad_reader_functor (ρ ρ' : out_param (Type u)) (n n' : Type u → Type u) := (map {α : Type u} : (∀ {m : Type u → Type u} [monad m], reader_t ρ m α → reader_t ρ' m α) → n α → n' α)

Instances
@[instance]
def monad_reader_adapter_trans {ρ ρ' : Type u} {m m' n n' : Type uType v} [monad_functor m m' n n'] [monad_reader_adapter ρ ρ' m m'] :

Equations
@[instance]
def reader_t.monad_reader_adapter {ρ ρ' : Type u} {m : Type uType v} [monad m] :
monad_reader_adapter ρ ρ' (reader_t ρ m) (reader_t ρ' m)

Equations
@[instance]
def reader_t.monad_run (ρ : Type u) (m : Type uType u_1) (out : out_param (Type uType u_1)) [monad_run out m] :
monad_run (λ (α : Type u), ρ → out α) (reader_t ρ m)

Equations