The Exception monad transformer using CPS style.
@[inline]
def
ExceptCpsT.run
{m : Type u → Type u_1}
{ε : Type u}
{α : Type u}
[Monad m]
(x : ExceptCpsT ε m α)
:
m (Except ε α)
Instances For
@[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 β
Instances For
@[inline]
def
ExceptCpsT.runCatch
{m : Type u_1 → Type u_2}
{α : Type u_1}
[Monad m]
(x : ExceptCpsT α m α)
:
m α
Instances For
@[always_inline]
instance
ExceptCpsT.instMonadExceptCpsT
{ε : Type u_1}
{m : Type u_1 → Type u_2}
:
Monad (ExceptCpsT ε m)
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)
@[inline]
def
ExceptCpsT.lift
{m : Type u_1 → Type u_2}
{α : Type u_1}
{ε : Type u_1}
[Monad m]
(x : m α)
:
ExceptCpsT ε m α
Instances For
instance
ExceptCpsT.instMonadLiftExceptCpsT
{m : Type u_1 → Type u_2}
{σ : Type u_1}
[Monad m]
:
MonadLift m (ExceptCpsT σ m)
instance
ExceptCpsT.instInhabitedExceptCpsT
{ε : Type u_1}
{m : Type u_1 → Type u_2}
{α : Type u_1}
[Inhabited ε]
:
Inhabited (ExceptCpsT ε m α)
@[simp]
theorem
ExceptCpsT.run_lift
{m : Type u → Type u_1}
{α : Type u}
{ε : Type u}
[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 : ε}
[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}
[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}
[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 : α}
[Monad m]
:
ExceptCpsT.runCatch (pure x) = pure x
@[simp]
theorem
ExceptCpsT.runCatch_lift
{m : Type u → Type u_1}
{α : Type u}
[Monad m]
[LawfulMonad m]
(x : m α)
:
@[simp]
theorem
ExceptCpsT.runCatch_throw
{m : Type u_1 → Type u_2}
{α : Type u_1}
{a : α}
[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}
[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}
[Monad m]
(e : β)
(f : α → ExceptCpsT β m β)
:
ExceptCpsT.runCatch (throw e >>= f) = pure e