mathlib documentation

core / init.control.reader

@[reducible]
def reader (ρ α : Type u) :
Type u
Equations
@[protected]
def reader_t.read {ρ : Type u} {m : Type uType v} [monad m] :
reader_t ρ m ρ
Equations
@[protected]
def reader_t.pure {ρ : Type u} {m : Type uType v} [monad m] {α : Type u} (a : α) :
reader_t ρ m α
Equations
@[protected]
def reader_t.bind {ρ : Type u} {m : Type uType v} [monad m] {α β : Type u} (x : reader_t ρ m α) (f : α → reader_t ρ m β) :
reader_t ρ m β
Equations
@[protected, instance]
def reader_t.monad {ρ : Type u} {m : Type uType v} [monad m] :
Equations
@[protected]
def reader_t.lift {ρ : Type u} {m : Type uType v} [monad m] {α : Type u} (a : m α) :
reader_t ρ m α
Equations
@[protected, instance]
def reader_t.has_monad_lift {ρ : Type u} (m : Type uType u_1) [monad m] :
Equations
@[protected]
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} (f : Π {α : Type u_1}, m αm' α) :
reader_t ρ m αreader_t ρ m' α
Equations
@[protected, 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
@[protected]
def reader_t.adapt {ρ : Type u} {m : Type uType v} [monad m] {ρ' : Type u} [monad m] {α : Type u} (f : ρ' → ρ) :
reader_t ρ m αreader_t ρ' m α
Equations
@[protected]
def reader_t.orelse {ρ : Type u} {m : Type uType v} [monad m] [alternative m] {α : Type u} (x₁ x₂ : reader_t ρ m α) :
reader_t ρ m α
Equations
@[protected]
def reader_t.failure {ρ : Type u} {m : Type uType v} [monad m] [alternative m] {α : Type u} :
reader_t ρ m α
Equations
@[protected, instance]
def reader_t.alternative {ρ : Type u} {m : Type uType v} [monad m] [alternative m] :
Equations
@[protected, 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)) (m : 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

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 of this typeclass
Instances of other typeclasses for monad_reader
  • monad_reader.has_sizeof_inst
@[protected, instance]
def monad_reader_trans {ρ : Type u} {m : Type uType v} {n : Type uType w} [monad_reader ρ m] [has_monad_lift m n] :
Equations
@[protected, instance]
def reader_t.monad_reader {ρ : Type u} {m : Type uType v} [monad m] :
Equations
@[class]
structure monad_reader_adapter (ρ ρ' : out_param (Type u)) (m m' : 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

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 of this typeclass
Instances of other typeclasses for monad_reader_adapter
  • monad_reader_adapter.has_sizeof_inst
@[protected, instance]
def monad_reader_adapter_trans {ρ ρ' : Type u} {m m' n n' : Type uType v} [monad_reader_adapter ρ ρ' m m'] [monad_functor m m' n n'] :
Equations
@[protected, 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
@[protected, 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