instance
ExceptT.instMonadFunctorExceptT
{ε : Type u}
{m : Type u → Type v}
:
MonadFunctor m (ExceptT ε m)
@[always_inline]
instance
instMonadExceptOfExceptT
(m : Type u → Type v)
(ε₁ : Type u)
(ε₂ : Type u)
[Monad m]
[MonadExceptOf ε₁ m]
:
MonadExceptOf ε₁ (ExceptT ε₂ m)
@[always_inline]
instance
instMonadExceptOfExceptT_1
(m : Type u → Type v)
(ε : Type u)
[Monad m]
:
MonadExceptOf ε (ExceptT ε m)
@[inline]
def
MonadExcept.orelse'
{ε : Type u}
{m : Type v → Type w}
[MonadExcept ε m]
{α : Type v}
(t₁ : m α)
(t₂ : m α)
(useFirstEx : optParam Bool true)
:
m α
Alternative orelse operator that allows to select which exception should be used.
The default is to use the first exception since the standard orelse
uses the second.
Instances For
def
liftExcept
{ε : Type u_1}
{m : Type u_2 → Type u_3}
{α : Type u_2}
[MonadExceptOf ε m]
[Pure m]
:
Except ε α → m α
Instances For
instance
instMonadControlExceptT
(ε : Type u)
(m : Type u → Type v)
[Monad m]
:
MonadControl m (ExceptT ε m)
tryFinally' x f
runsx
and then the "finally" computationf
. Whenx
succeeds witha : α
,f (some a)
is returned. Ifx
fails form
's definition of failure,f none
is returned. HencetryFinally'
can be thought of as performing the same role as afinally
block in an imperative programming language.
Instances
@[inline]
def
tryFinally
{m : Type u → Type v}
{α : Type u}
{β : Type u}
[MonadFinally m]
[Functor m]
(x : m α)
(finalizer : m β)
:
m α
Execute x
and then execute finalizer
even if x
threw an exception
Instances For
@[always_inline]
instance
ExceptT.finally
{m : Type u → Type v}
{ε : Type u}
[MonadFinally m]
[Monad m]
:
MonadFinally (ExceptT ε m)