Equations
- ExceptCpsT ε m α = ((β : Type u) → (α → m β) → (ε → m β) → m β)
@[inline]
def
ExceptCpsT.run
{m : Type u → Type u_1}
{ε : Type u}
{α : Type u}
[inst : Monad m]
(x : ExceptCpsT ε m α)
:
m (Except ε α)
Equations
- ExceptCpsT.run x = x (Except ε α) (fun a => pure (Except.ok a)) fun e => pure (Except.error e)
@[inline]
def
ExceptCpsT.runK
{m : Type u → Type u_1}
{β : Type u}
{ε : Type u}
{α : Type u}
(x : ExceptCpsT ε m α)
(s : ε)
(ok : α → m β)
(error : ε → m β)
:
m β
Equations
- ExceptCpsT.runK x s ok error = x β ok error
@[inline]
def
ExceptCpsT.runCatch
{m : Type u_1 → Type u_2}
{α : Type u_1}
[inst : Monad m]
(x : ExceptCpsT α m α)
:
m α
Equations
- ExceptCpsT.runCatch x = x α pure pure
instance
ExceptCpsT.instMonadExceptCpsT
{ε : Type u_1}
{m : Type u_1 → Type u_2}
:
Monad (ExceptCpsT ε m)
Equations
- ExceptCpsT.instMonadExceptCpsT = Monad.mk
noncomputable instance
ExceptCpsT.instLawfulMonadExceptCpsTInstMonadExceptCpsT
{σ : Type u_1}
{m : Type u_1 → Type u_2}
:
LawfulMonad (ExceptCpsT σ m)
instance
ExceptCpsT.instMonadExceptOfExceptCpsT
{ε : Type u_1}
{m : Type u_1 → Type u_2}
:
MonadExceptOf ε (ExceptCpsT ε m)
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_1 → Type u_2}
{α : Type u_1}
{ε : Type u_1}
[inst : Monad m]
(x : m α)
:
ExceptCpsT ε m α
Equations
- ExceptCpsT.lift x x k x = x >>= k
instance
ExceptCpsT.instMonadLiftExceptCpsT
{m : Type u_1 → Type u_2}
{σ : Type u_1}
[inst : Monad m]
:
MonadLift m (ExceptCpsT σ m)
Equations
- ExceptCpsT.instMonadLiftExceptCpsT = { monadLift := fun {α} => ExceptCpsT.lift }
instance
ExceptCpsT.instInhabitedExceptCpsT
{ε : Type u_1}
{m : Type u_1 → Type u_2}
{α : Type u_1}
[inst : Inhabited ε]
:
Inhabited (ExceptCpsT ε m α)
Equations
- ExceptCpsT.instInhabitedExceptCpsT = { default := fun x x_1 k₂ => k₂ default }
@[simp]
theorem
ExceptCpsT.run_pure
{m : Type u_1 → Type u_2}
{ε : Type u_1}
{α : Type u_1}
{x : α}
[inst : Monad m]
:
ExceptCpsT.run (pure x) = pure (Except.ok x)
@[simp]
theorem
ExceptCpsT.run_lift
{m : Type u → Type u_1}
{α : Type u}
{ε : Type u}
[inst : Monad m]
(x : m α)
:
ExceptCpsT.run (ExceptCpsT.lift x) = do
let a ← x
pure (Except.ok a)
@[simp]
theorem
ExceptCpsT.run_throw
{m : Type u_1 → Type u_2}
{ε : Type u_1}
{β : Type u_1}
{e : ε}
[inst : Monad m]
:
ExceptCpsT.run (throw e) = pure (Except.error e)
@[simp]
theorem
ExceptCpsT.run_bind_lift
{m : Type u_1 → Type u_2}
{α : Type u_1}
{ε : Type u_1}
{β : Type u_1}
[inst : Monad m]
(x : m α)
(f : α → ExceptCpsT ε m β)
:
ExceptCpsT.run (ExceptCpsT.lift x >>= f) = do
let a ← x
ExceptCpsT.run (f a)
@[simp]
theorem
ExceptCpsT.run_bind_throw
{m : Type u_1 → Type u_2}
{ε : Type u_1}
{α : Type u_1}
{β : Type u_1}
[inst : Monad m]
(e : ε)
(f : α → ExceptCpsT ε m β)
:
ExceptCpsT.run (throw e >>= f) = ExceptCpsT.run (throw e)
@[simp]
theorem
ExceptCpsT.runCatch_pure
{m : Type u_1 → Type u_2}
{α : Type u_1}
{x : α}
[inst : Monad m]
:
ExceptCpsT.runCatch (pure x) = pure x
@[simp]
theorem
ExceptCpsT.runCatch_lift
{m : Type u → Type u_1}
{α : Type u}
[inst : Monad m]
[inst : LawfulMonad m]
(x : m α)
:
@[simp]
theorem
ExceptCpsT.runCatch_throw
{m : Type u_1 → Type u_2}
{α : Type u_1}
{a : α}
[inst : Monad m]
:
ExceptCpsT.runCatch (throw a) = pure a
@[simp]
theorem
ExceptCpsT.runCatch_bind_lift
{m : Type u_1 → Type u_2}
{α : Type u_1}
{β : Type u_1}
[inst : Monad m]
(x : m α)
(f : α → ExceptCpsT β m β)
:
ExceptCpsT.runCatch (ExceptCpsT.lift x >>= f) = do
let a ← x
ExceptCpsT.runCatch (f a)
@[simp]
theorem
ExceptCpsT.runCatch_bind_throw
{m : Type u_1 → Type u_2}
{β : Type u_1}
{α : Type u_1}
[inst : Monad m]
(e : β)
(f : α → ExceptCpsT β m β)
:
ExceptCpsT.runCatch (throw e >>= f) = pure e