The Exception monad transformer using CPS style.
@[inline]
def
ExceptCpsT.run
{m : Type u → Type u_1}
{ε α : Type u}
[Monad m]
(x : ExceptCpsT ε m α)
:
m (Except ε α)
Use a monadic action that may throw an exception as an action that may return an exception's value.
Equations
Instances For
@[inline]
def
ExceptCpsT.runK
{m : Type u → Type u_1}
{β ε α : Type u}
(x : ExceptCpsT ε m α)
(s : ε)
(ok : α → m β)
(error : ε → m β)
:
m β
Use a monadic action that may throw an exception by providing explicit success and failure continuations.
Equations
Instances For
@[inline]
def
ExceptCpsT.runCatch
{m : Type u_1 → Type u_2}
{α : Type u_1}
[Monad m]
(x : ExceptCpsT α m α)
:
m α
Returns the value of a computation, forgetting whether it was an exception or a success.
This corresponds to early return.
Equations
Instances For
@[always_inline]
Equations
instance
ExceptCpsT.instLawfulMonad
{σ : Type u_1}
{m : Type u_1 → Type u_2}
:
LawfulMonad (ExceptCpsT σ m)
instance
ExceptCpsT.instMonadExceptOf
{ε : Type u_1}
{m : Type u_1 → Type u_2}
:
MonadExceptOf ε (ExceptCpsT ε m)
Equations
@[inline]
def
ExceptCpsT.lift
{m : Type u_1 → Type u_2}
{α ε : Type u_1}
[Monad m]
(x : m α)
:
ExceptCpsT ε m α
Run an action from the transformed monad in the exception monad.
Equations
Instances For
instance
ExceptCpsT.instMonadLiftOfMonad
{m : Type u_1 → Type u_2}
{σ : Type u_1}
[Monad m]
:
MonadLift m (ExceptCpsT σ m)
Equations
instance
ExceptCpsT.instInhabited
{ε : Type u_1}
{m : Type u_1 → Type u_2}
{α : Type u_1}
[Inhabited ε]
:
Inhabited (ExceptCpsT ε m α)
Equations
@[simp]
theorem
ExceptCpsT.runCatch_lift
{m : Type u → Type u_1}
{α : Type u}
[Monad m]
[LawfulMonad m]
(x : m α)
: