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 frunsxand then the "finally" computationf. Whenxsucceeds witha : α,f (some a)is returned. Ifxfails form's definition of failure,f noneis returned. HencetryFinally'can be thought of as performing the same role as afinallyblock 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)