# Documentation

Monad encapsulating continuation passing programming style, similar to Haskell's Cont, ContT and MonadCont: http://hackage.haskell.org/package/mtl-2.2.2/docs/Control-Monad-Cont.html

structure MonadCont.Label (α : Type w) (m : Type u → Type v) (β : Type u) :
Type (max v w)
• apply : αm β
Instances For
def MonadCont.goto {α : Type u_1} {β : Type u} {m : Type u → Type v} (f : ContT.Label α m β) (x : α) :
m β
Equations
• = f.apply x
Instances For
class MonadCont (m : Type u → Type v) :
Type (max (u + 1) v)
Instances
class LawfulMonadCont (m : Type u → Type v) [] [] extends :
Instances
theorem LawfulMonadCont.callCC_bind_right {m : Type u → Type v} [] [] [self : ] {α : Type u} {ω : Type u} {γ : Type u} (cmd : m α) (next : ContT.Label ω m γαm ω) :
(MonadCont.callCC fun (f : ContT.Label ω m γ) => cmd >>= next f) = do let xcmd MonadCont.callCC fun (f : ContT.Label ω m γ) => next f x
theorem LawfulMonadCont.callCC_bind_left {m : Type u → Type v} [] [] [self : ] {α : Type u} (β : Type u) (x : α) (dead : ContT.Label α m ββm α) :
(MonadCont.callCC fun (f : ContT.Label α m β) => >>= dead f) = pure x
theorem LawfulMonadCont.callCC_dummy {m : Type u → Type v} [] [] [self : ] {α : Type u} {β : Type u} (dummy : m α) :
(MonadCont.callCC fun (x : ContT.Label α m β) => dummy) = dummy
def ContT (r : Type u) (m : Type u → Type v) (α : Type w) :
Type (max v w)
Equations
• ContT r m α = ((αm r)m r)
Instances For
@[reducible, inline]
abbrev Cont (r : Type u) (α : Type w) :
Type (max u w)
Equations
Instances For
def ContT.run {r : Type u} {m : Type u → Type v} {α : Type w} :
ContT r m α(αm r)m r
Equations
• ContT.run = id
Instances For
def ContT.map {r : Type u} {m : Type u → Type v} {α : Type w} (f : m rm r) (x : ContT r m α) :
ContT r m α
Equations
Instances For
theorem ContT.run_contT_map_contT {r : Type u} {m : Type u → Type v} {α : Type w} (f : m rm r) (x : ContT r m α) :
(ContT.map f x).run = f x.run
def ContT.withContT {r : Type u} {m : Type u → Type v} {α : Type w} {β : Type w} (f : (βm r)αm r) (x : ContT r m α) :
ContT r m β
Equations
• = x (f g)
Instances For
theorem ContT.run_withContT {r : Type u} {m : Type u → Type v} {α : Type w} {β : Type w} (f : (βm r)αm r) (x : ContT r m α) :
(ContT.withContT f x).run = x.run f
theorem ContT.ext_iff {r : Type u} {m : Type u → Type v} {α : Type w} {x : ContT r m α} {y : ContT r m α} :
x = y ∀ (f : αm r), x.run f = y.run f
theorem ContT.ext {r : Type u} {m : Type u → Type v} {α : Type w} {x : ContT r m α} {y : ContT r m α} (h : ∀ (f : αm r), x.run f = y.run f) :
x = y
instance ContT.instMonad {r : Type u} {m : Type u → Type v} :
Equations
instance ContT.instLawfulMonad {r : Type u} {m : Type u → Type v} :
Equations
• =
def ContT.monadLift {r : Type u} {m : Type u → Type v} [] {α : Type u} :
m αContT r m α
Equations
Instances For
instance ContT.instMonadLiftOfMonad {r : Type u} {m : Type u → Type v} [] :
Equations
theorem ContT.monadLift_bind {r : Type u} {m : Type u → Type v} [] [] {α : Type u} {β : Type u} (x : m α) (f : αm β) :
instance ContT.instMonadCont {r : Type u} {m : Type u → Type v} :
Equations
• ContT.instMonadCont = { callCC := fun {α β : Type ?u.26} (f : ContT.Label α (ContT r m) βContT r m α) (g : αm r) => f { apply := fun (x : α) (x_1 : βm r) => g x } g }
instance ContT.instLawfulMonadCont {r : Type u} {m : Type u → Type v} :
Equations
• =
instance ContT.instMonadExcept {r : Type u} {m : Type u → Type v} (ε : Type u_1) [] :
Equations
• One or more equations did not get rendered due to their size.
def ExceptT.mkLabel {m : Type u → Type v} [] {α : Type u} {β : Type u} {ε : Type u} :
ContT.Label (Except ε α) m βContT.Label α (ExceptT ε m) β
Equations
Instances For
theorem ExceptT.goto_mkLabel {m : Type u → Type v} [] {α : Type u} {β : Type u} {ε : Type u} (x : ContT.Label (Except ε α) m β) (i : α) :
= ExceptT.mk (Except.ok <\$> ContT.goto x (Except.ok i))
def ExceptT.callCC {m : Type u → Type v} [] {ε : Type u} [] {α : Type u} {β : Type u} (f : ContT.Label α (ExceptT ε m) βExceptT ε m α) :
ExceptT ε m α
Equations
Instances For
instance instMonadContExceptT {m : Type u → Type v} [] {ε : Type u} [] :
Equations
• instMonadContExceptT = { callCC := fun {α β : Type ?u.30} => ExceptT.callCC }
instance instLawfulMonadContExceptT {m : Type u → Type v} [] {ε : Type u} [] [] :
Equations
• =
def OptionT.mkLabel {m : Type u → Type v} [] {α : Type u} {β : Type u} :
ContT.Label (Option α) m βContT.Label α (OptionT m) β
Equations
Instances For
theorem OptionT.goto_mkLabel {m : Type u → Type v} [] {α : Type u} {β : Type u} (x : ContT.Label (Option α) m β) (i : α) :
= OptionT.mk do let aContT.goto x (some i) pure (some a)
def OptionT.callCC {m : Type u → Type v} [] [] {α : Type u} {β : Type u} (f : ContT.Label α (OptionT m) βOptionT m α) :
OptionT m α
Equations
Instances For
instance instMonadContOptionT {m : Type u → Type v} [] [] :
Equations
• instMonadContOptionT = { callCC := fun {α β : Type ?u.25} => OptionT.callCC }
instance instLawfulMonadContOptionT {m : Type u → Type v} [] [] [] :
Equations
• =
def WriterT.mkLabel {m : Type u → Type v} [] {α : Type u_1} {β : Type u} {ω : Type u} [] :
ContT.Label (α × ω) m βContT.Label α (WriterT ω m) β
Equations
Instances For
def WriterT.mkLabel' {m : Type u → Type v} [] {α : Type u_1} {β : Type u} {ω : Type u} [] :
ContT.Label (α × ω) m βContT.Label α (WriterT ω m) β
Equations
Instances For
theorem WriterT.goto_mkLabel {m : Type u → Type v} [] {α : Type u_1} {β : Type u} {ω : Type u} [] (x : ContT.Label (α × ω) m β) (i : α) :
theorem WriterT.goto_mkLabel' {m : Type u → Type v} [] {α : Type u_1} {β : Type u} {ω : Type u} [] (x : ContT.Label (α × ω) m β) (i : α) :
= monadLift (ContT.goto x (i, 1))
def WriterT.callCC {m : Type u → Type v} [] [] {α : Type u} {β : Type u} {ω : Type u} [] (f : ContT.Label α (WriterT ω m) βWriterT ω m α) :
WriterT ω m α
Equations
Instances For
def WriterT.callCC' {m : Type u → Type v} [] [] {α : Type u} {β : Type u} {ω : Type u} [] (f : ContT.Label α (WriterT ω m) βWriterT ω m α) :
WriterT ω m α
Equations
Instances For
instance instMonadContWriterTOfMonadOfEmptyCollection {m : Type u → Type v} (ω : Type u) [] [] [] :
Equations
• = { callCC := fun {α β : Type ?u.35} => WriterT.callCC }
instance instMonadContWriterTOfMonadOfMonoid {m : Type u → Type v} (ω : Type u) [] [] [] :
Equations
• = { callCC := fun {α β : Type ?u.35} => WriterT.callCC' }
def StateT.mkLabel {m : Type u → Type v} {α : Type u} {β : Type u} {σ : Type u} :
ContT.Label (α × σ) m (β × σ)ContT.Label α (StateT σ m) β
Equations
Instances For
theorem StateT.goto_mkLabel {m : Type u → Type v} {α : Type u} {β : Type u} {σ : Type u} (x : ContT.Label (α × σ) m (β × σ)) (i : α) :
= StateT.mk fun (s : σ) => ContT.goto x (i, s)
def StateT.callCC {m : Type u → Type v} {σ : Type u} [] {α : Type u} {β : Type u} (f : ContT.Label α (StateT σ m) βStateT σ m α) :
StateT σ m α
Equations
Instances For
instance instMonadContStateT {m : Type u → Type v} {σ : Type u} [] :
Equations
• instMonadContStateT = { callCC := fun {α β : Type ?u.25} => StateT.callCC }
instance instLawfulMonadContStateT {m : Type u → Type v} {σ : Type u} [] [] [] :
Equations
• =
def ReaderT.mkLabel {m : Type u → Type v} {α : Type u_1} {β : Type u} (ρ : Type u) :
ContT.Label α m βContT.Label α (ReaderT ρ m) β
Equations
Instances For
theorem ReaderT.goto_mkLabel {m : Type u → Type v} {α : Type u_1} {ρ : Type u} {β : Type u} (x : ContT.Label α m β) (i : α) :
def ReaderT.callCC {m : Type u → Type v} {ε : Type u} [] {α : Type u} {β : Type u} (f : ContT.Label α (ReaderT ε m) βReaderT ε m α) :
Equations
Instances For
instance instMonadContReaderT {m : Type u → Type v} {ρ : Type u} [] :
Equations