Documentation

Init.Control.ExceptCps

noncomputable def ExceptCpsT (ε : Type u) (m : Type uType v) (α : Type u) :
Type (max (u + 1) v)
Equations
  • ExceptCpsT ε m α = ((β : Type u) → (αm β) → (εm β) → m β)
@[inline]
def ExceptCpsT.run {m : Type uType u_1} {ε : Type u} {α : Type u} [inst : Monad m] (x : ExceptCpsT ε m α) :
m (Except ε α)
Equations
@[inline]
def ExceptCpsT.runK {m : Type uType u_1} {β : Type u} {ε : Type u} {α : Type u} (x : ExceptCpsT ε m α) (s : ε) (ok : αm β) (error : εm β) :
m β
Equations
@[inline]
def ExceptCpsT.runCatch {m : Type u_1Type u_2} {α : Type u_1} [inst : Monad m] (x : ExceptCpsT α m α) :
m α
Equations
instance ExceptCpsT.instMonadExceptCpsT {ε : Type u_1} {m : Type u_1Type u_2} :
Equations
  • ExceptCpsT.instMonadExceptCpsT = Monad.mk
instance ExceptCpsT.instMonadExceptOfExceptCpsT {ε : Type u_1} {m : Type u_1Type u_2} :
Equations
  • ExceptCpsT.instMonadExceptOfExceptCpsT = { throw := fun {α} e x x_1 k => k e, tryCatch := fun {α} x handle x_1 k₁ k₂ => x x_1 k₁ fun e => handle e x_1 k₁ k₂ }
@[inline]
def ExceptCpsT.lift {m : Type u_1Type u_2} {α : Type u_1} {ε : Type u_1} [inst : Monad m] (x : m α) :
ExceptCpsT ε m α
Equations
instance ExceptCpsT.instMonadLiftExceptCpsT {m : Type u_1Type u_2} {σ : Type u_1} [inst : Monad m] :
Equations
  • ExceptCpsT.instMonadLiftExceptCpsT = { monadLift := fun {α} => ExceptCpsT.lift }
instance ExceptCpsT.instInhabitedExceptCpsT {ε : Type u_1} {m : Type u_1Type u_2} {α : Type u_1} [inst : Inhabited ε] :
Equations
  • ExceptCpsT.instInhabitedExceptCpsT = { default := fun x x_1 k₂ => k₂ default }
@[simp]
theorem ExceptCpsT.run_pure {m : Type u_1Type u_2} {ε : Type u_1} {α : Type u_1} {x : α} [inst : Monad m] :
@[simp]
theorem ExceptCpsT.run_lift {m : Type uType u_1} {α : Type u} {ε : Type u} [inst : Monad m] (x : m α) :
@[simp]
theorem ExceptCpsT.run_throw {m : Type u_1Type u_2} {ε : Type u_1} {β : Type u_1} {e : ε} [inst : Monad m] :
@[simp]
theorem ExceptCpsT.run_bind_lift {m : Type u_1Type u_2} {α : Type u_1} {ε : Type u_1} {β : Type u_1} [inst : Monad m] (x : m α) (f : αExceptCpsT ε m β) :
@[simp]
theorem ExceptCpsT.run_bind_throw {m : Type u_1Type u_2} {ε : Type u_1} {α : Type u_1} {β : Type u_1} [inst : Monad m] (e : ε) (f : αExceptCpsT ε m β) :
@[simp]
theorem ExceptCpsT.runCatch_pure {m : Type u_1Type u_2} {α : Type u_1} {x : α} [inst : Monad m] :
@[simp]
theorem ExceptCpsT.runCatch_lift {m : Type uType u_1} {α : Type u} [inst : Monad m] [inst : LawfulMonad m] (x : m α) :
@[simp]
theorem ExceptCpsT.runCatch_throw {m : Type u_1Type u_2} {α : Type u_1} {a : α} [inst : Monad m] :
@[simp]
theorem ExceptCpsT.runCatch_bind_lift {m : Type u_1Type u_2} {α : Type u_1} {β : Type u_1} [inst : Monad m] (x : m α) (f : αExceptCpsT β m β) :
@[simp]
theorem ExceptCpsT.runCatch_bind_throw {m : Type u_1Type u_2} {β : Type u_1} {α : Type u_1} [inst : Monad m] (e : β) (f : αExceptCpsT β m β) :