mathlib documentation

control.monad.cont

structure monad_cont.label (α : Type w) (m : Type uType v) (β : Type u) :
Type (max v w)
  • apply : α → m β
def monad_cont.goto {α : Type u_1} {β : Type u} {m : Type uType v} (f : monad_cont.label α m β) (x : α) :
m β
Equations
@[class]
structure monad_cont (m : Type uType v) :
Type (max (u+1) v)
Instances
@[class]
structure is_lawful_monad_cont (m : Type uType v) [monad m] [monad_cont m] :
Type
Instances
def cont_t (r : Type u) (m : Type uType v) (α : Type w) :
Type (max w v)
Equations
  • cont_t r m α = ((α → m r)m r)
def cont (r : Type u) (α : Type w) :
Type (max w u)
Equations
def cont_t.run {r : Type u} {m : Type uType v} {α : Type w} :
cont_t r m α(α → m r)m r
Equations
def cont_t.map {r : Type u} {m : Type uType v} {α : Type w} (f : m rm r) (x : cont_t r m α) :
cont_t r m α
Equations
theorem cont_t.run_cont_t_map_cont_t {r : Type u} {m : Type uType v} {α : Type w} (f : m rm r) (x : cont_t r m α) :
(cont_t.map f x).run = f x.run
def cont_t.with_cont_t {r : Type u} {m : Type uType v} {α β : Type w} (f : (β → m r)α → m r) (x : cont_t r m α) :
cont_t r m β
Equations
theorem cont_t.run_with_cont_t {r : Type u} {m : Type uType v} {α β : Type w} (f : (β → m r)α → m r) (x : cont_t r m α) :
@[ext]
theorem cont_t.ext {r : Type u} {m : Type uType v} {α : Type w} {x y : cont_t r m α} (h : ∀ (f : α → m r), x.run f = y.run f) :
x = y
@[instance]
def cont_t.monad {r : Type u} {m : Type uType v} :
Equations
@[instance]
def cont_t.is_lawful_monad {r : Type u} {m : Type uType v} :
def cont_t.monad_lift {r : Type u} {m : Type uType v} [monad m] {α : Type u} :
m αcont_t r m α
Equations
@[instance]
def cont_t.has_monad_lift {r : Type u} {m : Type uType v} [monad m] :
Equations
theorem cont_t.monad_lift_bind {r : Type u} {m : Type uType v} [monad m] [is_lawful_monad m] {α β : Type u} (x : m α) (f : α → m β) :
@[instance]
def cont_t.monad_cont {r : Type u} {m : Type uType v} :
Equations
@[instance]
def cont_t.is_lawful_monad_cont {r : Type u} {m : Type uType v} :
Equations
@[instance]
def cont_t.monad_except {r : Type u} {m : Type uType v} (ε : out_param (Type u_1)) [monad_except ε m] :
Equations
@[instance]
def cont_t.monad_run {r : Type u} {m : Type uType v} :
monad_run (λ (α : Type u), (α → m r)ulift (m r)) (cont_t r m)
Equations
def except_t.mk_label {m : Type uType v} [monad m] {α β ε : Type u} :
monad_cont.label (except ε α) m βmonad_cont.label α (except_t ε m) β
Equations
theorem except_t.goto_mk_label {m : Type uType v} [monad m] {α β ε : Type u} (x : monad_cont.label (except ε α) m β) (i : α) :
def except_t.call_cc {m : Type uType v} [monad m] {ε : Type u} [monad_cont m] {α β : Type u} (f : monad_cont.label α (except_t ε m) βexcept_t ε m α) :
except_t ε m α
Equations
@[instance]
def except_t.monad_cont {m : Type uType v} [monad m] {ε : Type u} [monad_cont m] :
Equations
def option_t.mk_label {m : Type uType v} [monad m] {α β : Type u} :
Equations
theorem option_t.goto_mk_label {m : Type uType v} [monad m] {α β : Type u} (x : monad_cont.label (option α) m β) (i : α) :
def option_t.call_cc {m : Type uType v} [monad m] [monad_cont m] {α β : Type u} (f : monad_cont.label α (option_t m) βoption_t m α) :
Equations
@[instance]
def option_t.monad_cont {m : Type uType v} [monad m] [monad_cont m] :
Equations
def writer_t.mk_label {m : Type uType v} [monad m] {α : Type u_1} {β ω : Type u} [has_one «ω»] :
monad_cont.label × «ω») m βmonad_cont.label α (writer_t «ω» m) β
Equations
theorem writer_t.goto_mk_label {m : Type uType v} [monad m] {α : Type u_1} {β ω : Type u} [has_one «ω»] (x : monad_cont.label × «ω») m β) (i : α) :
def writer_t.call_cc {m : Type uType v} [monad m] [monad_cont m] {α β ω : Type u} [has_one «ω»] (f : monad_cont.label α (writer_t «ω» m) βwriter_t «ω» m α) :
writer_t «ω» m α
Equations
@[instance]
def writer_t.monad_cont {m : Type uType v} [monad m] (ω : Type u) [monad m] [has_one «ω»] [monad_cont m] :
monad_cont (writer_t «ω» m)
Equations
def state_t.mk_label {m : Type uType v} [monad m] {α β σ : Type u} :
monad_cont.label × σ) m × σ)monad_cont.label α (state_t σ m) β
Equations
theorem state_t.goto_mk_label {m : Type uType v} [monad m] {α β σ : Type u} (x : monad_cont.label × σ) m × σ)) (i : α) :
monad_cont.goto (state_t.mk_label x) i = λ (s : σ), monad_cont.goto x (i, s)
def state_t.call_cc {m : Type uType v} [monad m] {σ : Type u} [monad_cont m] {α β : Type u} (f : monad_cont.label α (state_t σ m) βstate_t σ m α) :
state_t σ m α
Equations
@[instance]
def state_t.monad_cont {m : Type uType v} [monad m] {σ : Type u} [monad_cont m] :
Equations
def reader_t.mk_label {m : Type uType v} [monad m] {α : Type u_1} {β : Type u} (ρ : Type u) :
monad_cont.label α m βmonad_cont.label α (reader_t ρ m) β
Equations
theorem reader_t.goto_mk_label {m : Type uType v} [monad m] {α : Type u_1} {ρ β : Type u} (x : monad_cont.label α m β) (i : α) :
def reader_t.call_cc {m : Type uType v} [monad m] {ε : Type u} [monad_cont m] {α β : Type u} (f : monad_cont.label α (reader_t ε m) βreader_t ε m α) :
reader_t ε m α
Equations
@[instance]
def reader_t.monad_cont {m : Type uType v} [monad m] {ρ : Type u} [monad_cont m] :
Equations
def cont_t.equiv {m₁ : Type u₀Type v₀} {m₂ : Type u₁Type v₁} {α₁ r₁ : Type u₀} {α₂ r₂ : Type u₁} (F : m₁ r₁ m₂ r₂) (G : α₁ α₂) :
cont_t r₁ m₁ α₁ cont_t r₂ m₂ α₂

reduce the equivalence between two continuation passing monads to the equivalence between their underlying monad

Equations