mathlib3 documentation

control.monad.cont

source
structure monad_cont.label (α : Type w) (m : Type u → Type v) (β : Type u) :
Type (max v w)
  • apply : α → m β
Instances for monad_cont.label
  • monad_cont.label.has_sizeof_inst
source
def monad_cont.goto {α : Type u_1} {β : Type u} {m : Type u → Type v} (f : monad_cont.label α m β) (x : α) :
m β
Equations
source
@[class]
structure monad_cont (m : Type u → Type v) :
Type (max (u+1) v)
Instances of this typeclass
Instances of other typeclasses for monad_cont
  • monad_cont.has_sizeof_inst
source
@[class]
structure is_lawful_monad_cont (m : Type u → Type v) [monad m] [monad_cont m] :
Type
Instances of this typeclass
Instances of other typeclasses for is_lawful_monad_cont
  • is_lawful_monad_cont.has_sizeof_inst
source
def cont_t (r : Type u) (m : Type u → Type v) (α : Type w) :
Type (max w v)
Equations
Instances for cont_t
source
@[reducible]
def cont (r : Type u) (α : Type w) :
Type (max w u)
Equations
source
def cont_t.run {r : Type u} {m : Type u → Type v} {α : Type w} :
cont_t r m α → (α → m r) → m r
Equations
source
def cont_t.map {r : Type u} {m : Type u → Type v} {α : Type w} (f : m r → m r) (x : cont_t r m α) :
cont_t r m α
Equations
source
theorem cont_t.run_cont_t_map_cont_t {r : Type u} {m : Type u → Type v} {α : Type w} (f : m r → m r) (x : cont_t r m α) :
(cont_t.map f x).run = f ∘ x.run
source
def cont_t.with_cont_t {r : Type u} {m : Type u → Type v} {α β : Type w} (f : (β → m r) → α → m r) (x : cont_t r m α) :
cont_t r m β
Equations
source
theorem cont_t.run_with_cont_t {r : Type u} {m : Type u → Type v} {α β : Type w} (f : (β → m r) → α → m r) (x : cont_t r m α) :
(cont_t.with_cont_t f x).run = x.run ∘ f
source
@[protected, ext]
theorem cont_t.ext {r : Type u} {m : Type u → Type v} {α : Type w} {x y : cont_t r m α} (h : ∀ (f : α → m r), x.run f = y.run f) :
x = y
source
@[protected, instance]
def cont_t.monad {r : Type u} {m : Type u → Type v} :
monad (cont_t r m)
Equations
source
@[protected, instance]
def cont_t.is_lawful_monad {r : Type u} {m : Type u → Type v} :
is_lawful_monad (cont_t r m)
source
def cont_t.monad_lift {r : Type u} {m : Type u → Type v} [monad m] {α : Type u} :
m α → cont_t r m α
Equations
source
@[protected, instance]
def cont_t.has_monad_lift {r : Type u} {m : Type u → Type v} [monad m] :
has_monad_lift m (cont_t r m)
Equations
source
theorem cont_t.monad_lift_bind {r : Type u} {m : Type u → Type v} [monad m] [is_lawful_monad m] {α β : Type u} (x : m α) (f : α → m β) :
cont_t.monad_lift (x >>= f) = cont_t.monad_lift x >>= cont_t.monad_lift ∘ f
source
@[protected, instance]
def cont_t.monad_cont {r : Type u} {m : Type u → Type v} :
monad_cont (cont_t r m)
Equations
source
@[protected, instance]
def cont_t.is_lawful_monad_cont {r : Type u} {m : Type u → Type v} :
is_lawful_monad_cont (cont_t r m)
Equations
source
@[protected, instance]
def cont_t.monad_except {r : Type u} {m : Type u → Type v} (ε : out_param (Type u_1)) [monad_except ε m] :
monad_except ε (cont_t r m)
Equations
source
@[protected, instance]
def cont_t.monad_run {r : Type u} {m : Type u → Type v} :
monad_run (λ (α : Type u), (α → m r) → ulift (m r)) (cont_t r m)
Equations
source
def except_t.mk_label {m : Type u → Type v} [monad m] {α β ε : Type u} :
monad_cont.label (except ε α) m β → monad_cont.label α (except_t ε m) β
Equations
source
theorem except_t.goto_mk_label {m : Type u → Type v} [monad m] {α β ε : Type u} (x : monad_cont.label (except ε α) m β) (i : α) :
monad_cont.goto (except_t.mk_label x) i = ⟨except.ok <$> monad_cont.goto x (except.ok i)⟩
source
def except_t.call_cc {m : Type u → Type v} [monad m] {ε : Type u} [monad_cont m] {α β : Type u} (f : monad_cont.label α (except_t ε m) β → except_t ε m α) :
except_t ε m α
Equations
source
@[protected, instance]
def except_t.monad_cont {m : Type u → Type v} [monad m] {ε : Type u} [monad_cont m] :
monad_cont (except_t ε m)
Equations
source
@[protected, instance]
def except_t.is_lawful_monad_cont {m : Type u → Type v} [monad m] {ε : Type u} [monad_cont m] [is_lawful_monad_cont m] :
is_lawful_monad_cont (except_t ε m)
Equations
source
def option_t.mk_label {m : Type u → Type v} [monad m] {α β : Type u} :
monad_cont.label (option α) m β → monad_cont.label α (option_t m) β
Equations
source
theorem option_t.goto_mk_label {m : Type u → Type v} [monad m] {α β : Type u} (x : monad_cont.label (option α) m β) (i : α) :
monad_cont.goto (option_t.mk_label x) i = {run := option.some <$> monad_cont.goto x (option.some i)}
source
def option_t.call_cc {m : Type u → Type v} [monad m] [monad_cont m] {α β : Type u} (f : monad_cont.label α (option_t m) β → option_t m α) :
option_t m α
Equations
source
@[protected, instance]
def option_t.monad_cont {m : Type u → Type v} [monad m] [monad_cont m] :
monad_cont (option_t m)
Equations
source
@[protected, instance]
def option_t.is_lawful_monad_cont {m : Type u → Type v} [monad m] [monad_cont m] [is_lawful_monad_cont m] :
is_lawful_monad_cont (option_t m)
Equations
source
def writer_t.mk_label {m : Type u → Type v} [monad m] {α : Type u_1} {β ω : Type u} [has_one ω] :
monad_cont.label (α × ω) m β → monad_cont.label α (writer_t ω m) β
Equations
source
theorem writer_t.goto_mk_label {m : Type u → Type v} [monad m] {α : Type u_1} {β ω : Type u} [has_one ω] (x : monad_cont.label (α × ω) m β) (i : α) :
monad_cont.goto (writer_t.mk_label x) i = has_monad_lift_t.monad_lift (monad_cont.goto x (i, 1))
source
def writer_t.call_cc {m : Type u → Type v} [monad m] [monad_cont m] {α β ω : Type u} [has_one ω] (f : monad_cont.label α (writer_t ω m) β → writer_t ω m α) :
writer_t ω m α
Equations
source
@[protected, instance]
def writer_t.monad_cont {m : Type u → Type v} [monad m] (ω : Type u) [monad m] [has_one ω] [monad_cont m] :
monad_cont (writer_t ω m)
Equations
source
def state_t.mk_label {m : Type u → Type v} [monad m] {α β σ : Type u} :
monad_cont.label (α × σ) m (β × σ) → monad_cont.label α (state_t σ m) β
Equations
source
theorem state_t.goto_mk_label {m : Type u → Type 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)⟩
source
def state_t.call_cc {m : Type u → Type v} [monad m] {σ : Type u} [monad_cont m] {α β : Type u} (f : monad_cont.label α (state_t σ m) β → state_t σ m α) :
state_t σ m α
Equations
source
@[protected, instance]
def state_t.monad_cont {m : Type u → Type v} [monad m] {σ : Type u} [monad_cont m] :
monad_cont (state_t σ m)
Equations
source
@[protected, instance]
def state_t.is_lawful_monad_cont {m : Type u → Type v} [monad m] {σ : Type u} [monad_cont m] [is_lawful_monad_cont m] :
is_lawful_monad_cont (state_t σ m)
Equations
source
def reader_t.mk_label {m : Type u → Type v} [monad m] {α : Type u_1} {β : Type u} (ρ : Type u) :
monad_cont.label α m β → monad_cont.label α (reader_t ρ m) β
Equations
source
theorem reader_t.goto_mk_label {m : Type u → Type v} [monad m] {α : Type u_1} {ρ β : Type u} (x : monad_cont.label α m β) (i : α) :
monad_cont.goto (reader_t.mk_label ρ x) i = has_monad_lift_t.monad_lift (monad_cont.goto x i)
source
def reader_t.call_cc {m : Type u → Type v} [monad m] {ε : Type u} [monad_cont m] {α β : Type u} (f : monad_cont.label α (reader_t ε m) β → reader_t ε m α) :
reader_t ε m α
Equations
source
@[protected, instance]
def reader_t.monad_cont {m : Type u → Type v} [monad m] {ρ : Type u} [monad_cont m] :
monad_cont (reader_t ρ m)
Equations
source
@[protected, instance]
def reader_t.is_lawful_monad_cont {m : Type u → Type v} [monad m] {ρ : Type u} [monad_cont m] [is_lawful_monad_cont m] :
is_lawful_monad_cont (reader_t ρ m)
Equations
source
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