# mathlibdocumentation

structure writer_t (ω : Type u) (m : Type uType v) (α : Type u) :
Type (max u v)
• run : m × «ω»)
def writer (ω α : Type u) :
Type u
Equations
@[ext]
theorem writer_t.ext {ω : Type u} {m : Type uType v} [monad m] {α : Type u} (x x' : writer_t «ω» m α) (h : x.run = x'.run) :
x = x'
def writer_t.tell {ω : Type u} {m : Type uType v} [monad m] (w : «ω») :
writer_t «ω» m punit
Equations
def writer_t.listen {ω : Type u} {m : Type uType v} [monad m] {α : Type u} :
writer_t «ω» m αwriter_t «ω» m × «ω»)
Equations
def writer_t.pass {ω : Type u} {m : Type uType v} [monad m] {α : Type u} :
writer_t «ω» m × («ω» → «ω»))writer_t «ω» m α
Equations
def writer_t.pure {ω : Type u} {m : Type uType v} [monad m] {α : Type u} [has_one «ω»] (a : α) :
writer_t «ω» m α
Equations
def writer_t.bind {ω : Type u} {m : Type uType v} [monad m] {α β : Type u} [has_mul «ω»] (x : writer_t «ω» m α) (f : α → writer_t «ω» m β) :
writer_t «ω» m β
Equations
@[instance]
def writer_t.monad {ω : Type u} {m : Type uType v} [monad m] [has_one «ω»] [has_mul «ω»] :
Equations
@[instance]
def writer_t.is_lawful_monad {ω : Type u} {m : Type uType v} [monad m] [monoid «ω»]  :
def writer_t.lift {ω : Type u} {m : Type uType v} [monad m] {α : Type u} [has_one «ω»] (a : m α) :
writer_t «ω» m α
Equations
@[instance]
def writer_t.has_monad_lift {ω : Type u} (m : Type uType u_1) [monad m] [has_one «ω»] :
(writer_t «ω» m)
Equations
def writer_t.monad_map {ω : Type u} {m : Type uType u_1} {m' : Type uType u_2} [monad m] [monad m'] {α : Type u} (f : Π {α : Type u}, m αm' α) :
writer_t «ω» m αwriter_t «ω» m' α
Equations
@[instance]
def writer_t.monad_functor {ω : Type u} (m m' : Type uType u_1) [monad m] [monad m'] :
m' (writer_t «ω» m) (writer_t «ω» m')
Equations
def writer_t.adapt {ω : Type u} {m : Type uType v} [monad m] {ω' α : Type u} (f : «ω» → ω') :
writer_t «ω» m αwriter_t ω' m α
Equations
@[instance]
def writer_t.monad_except {ω : Type u} {m : Type uType v} [monad m] (ε : out_param (Type u_1)) [has_one «ω»] [monad m] [ m] :
(writer_t «ω» m)
Equations
@[class]
structure monad_writer (ω : out_param (Type u)) (m : Type uType v) :
Type (max (u+1) v)
• tell : «ω» →
• listen : Π {α : Type ?}, m αm × «ω»)
• pass : Π {α : Type ?}, m × («ω» → «ω»))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
@[instance]
def writer_t.monad_writer {ω : Type u} {m : Type uType v} [monad m] :
Equations
@[instance]
Equations
• reader_t.monad_writer = {tell := λ (x : «ω»), monad_lift (tell x), listen := λ (α : Type u) (_x : m α), reader_t.monad_writer._match_1 α _x, pass := λ (α : Type u) (_x : m × («ω» → «ω»))), reader_t.monad_writer._match_2 α _x}
• reader_t.monad_writer._match_1 α cmd⟩ = λ (r : ρ), listen (cmd r)
• reader_t.monad_writer._match_2 α cmd⟩ = λ (r : ρ), pass (cmd r)
def swap_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} :
× β) × γ× γ) × β
Equations
@[instance]
def state_t.monad_writer {ω σ : Type u} {m : Type uType v} [monad m] [monad_writer «ω» m] :
Equations
def except_t.pass_aux {ε : Type u_1} {α : Type u_2} {ω : Type u_3} :
× («ω» → «ω»)) α × («ω» → «ω»)
Equations
@[instance]
def except_t.monad_writer {ω ε : Type u} {m : Type uType v} [monad m] [monad_writer «ω» m] :
Equations
def option_t.pass_aux {α : Type u_1} {ω : Type u_2} :
option × («ω» → «ω»)) × («ω» → «ω»)
Equations
@[instance]
def option_t.monad_writer {ω : Type u} {m : Type uType v} [monad m] [monad_writer «ω» m] :
Equations
@[class]
structure monad_writer_adapter (ω ω' : out_param (Type u)) (m m' : Type uType v) :
Type (max (u+1) v)
• adapt_writer : Π {α : Type ?}, («ω» → ω')m αm' α

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
@[nolint, instance]
def monad_writer_adapter_trans {ω ω' : Type u} {m m' n n' : Type uType v} [ ω' m m'] [ m' n n'] :
ω' n n'

Transitivity.

This instance generates the type-class problem with a metavariable argument (which is why this is marked as [nolint dangerous_instance]). Currently that is not a problem, as there are almost no instances of monad_functor or monad_writer_adapter.

Equations
@[instance]