# mathlib3documentation

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

Instances for reader_t
@[reducible]
def reader (ρ α : Type u) :
Equations
@[protected]
m ρ
Equations
@[protected]
def reader_t.pure {ρ : Type u} {m : Type u Type v} [monad m] {α : Type u} (a : α) :
m α
Equations
• = λ (r : ρ),
@[protected]
def reader_t.bind {ρ : Type u} {m : Type u Type v} [monad m] {α β : Type u} (x : m α) (f : α m β) :
m β
Equations
@[protected, instance]
Equations
@[protected]
def reader_t.lift {ρ : Type u} {m : Type u Type v} [monad m] {α : Type u} (a : m α) :
m α
Equations
• = λ (r : ρ), a
@[protected, instance]
Equations
@[protected]
def reader_t.monad_map {ρ : Type u_1} {m : Type u_1 Type u_2} {m' : Type u_1 Type u_3} [monad m] [monad m'] {α : Type u_1} (f : Π {α : Type u_1}, m α m' α) :
m α m' α
Equations
• = λ (x : m α), λ (r : ρ), f (x.run r)
@[protected, instance]
Equations
@[protected]
def reader_t.adapt {ρ : Type u} {m : Type u Type v} [monad m] {ρ' : Type u} [monad m] {α : Type u} (f : ρ' ρ) :
m α reader_t ρ' m α
Equations
• = λ (x : m α), λ (r : ρ'), x.run (f r)
@[protected]
def reader_t.orelse {ρ : Type u} {m : Type u Type v} [monad m] [alternative m] {α : Type u} (x₁ x₂ : m α) :
m α
Equations
@[protected]
def reader_t.failure {ρ : Type u} {m : Type u Type v} [monad m] [alternative m] {α : Type u} :
m α
Equations
@[protected, instance]
def reader_t.alternative {ρ : Type u} {m : Type u Type v} [monad m] [alternative m] :
Equations
@[protected, instance]
def reader_t.monad_except {ρ : Type u} {m : Type u Type v} [monad m] (ε : out_param (Type u_1)) [monad m] [ m] :
Equations
@[class]
structure monad_reader (ρ : out_param (Type u)) (m : Type u Type v) :

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
@[protected, instance]
def monad_reader_trans {ρ : Type u} {m : Type u Type v} {n : Type u Type w} [ m] [ n] :
n
Equations
@[protected, instance]
Equations
@[class]
Type (max (u+1) v)

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