mathlib documentation

control.monad.cont

structure monad_cont.label  :
Type w(Type uType v)Type uType (max v w)
  • apply : α → m β

def monad_cont.goto {α : Type u_1} {β : Type u} {m : Type uType v} :
monad_cont.label α m βα → m β

Equations
@[class]
structure monad_cont  :
(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  :
Type u(Type uType v)Type wType (max w v)

Equations
  • cont_t r m α = ((α → m r)m r)
def cont  :
Type uType wType (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} :
(m rm r)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} :
((β → m r)α → m r)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 α} :
(∀ (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} :
(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} :
(monad_cont.label α (option_t m) β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 «ω»] :
(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} :
(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] :
monad_cont (state_t «σ» m)

Equations
@[instance]
def state_t.is_lawful_monad_cont {m : Type uType v} [monad m] {σ : Type u} [monad_cont m] [is_lawful_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} :
(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₁} :
m₁ r₁ m₂ r₂α₁ α₂cont_t r₁ m₁ α₁ cont_t r₂ m₂ α₂

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

Equations