# Documentation

Init.Control.Except

@[inline]
def Except.pure {ε : Type u} {α : Type u_1} (a : α) :
Except ε α
Equations
@[inline]
def Except.map {ε : Type u} {α : Type u_1} {β : Type u_2} (f : αβ) :
Except ε αExcept ε β
Equations
@[simp]
theorem Except.map_id {ε : Type u} {α : Type u_1} :
= id
@[inline]
def Except.mapError {ε : Type u} {ε' : Type u_1} {α : Type u_2} (f : εε') :
Except ε αExcept ε' α
Equations
@[inline]
def Except.bind {ε : Type u} {α : Type u_1} {β : Type u_2} (ma : Except ε α) (f : αExcept ε β) :
Except ε β
Equations
@[inline]
def Except.toBool {ε : Type u} {α : Type u_1} :
Except ε αBool

Returns true if the value is Except.ok, false otherwise.

Equations
• = match x with | => true | => false
@[inline]
abbrev Except.isOk {ε : Type u} {α : Type u_1} :
Except ε αBool
Equations
• Except.isOk = Except.toBool
@[inline]
def Except.toOption {ε : Type u} {α : Type u_1} :
Except ε α
Equations
• = match x with | => some a | => none
@[inline]
def Except.tryCatch {ε : Type u} {α : Type u_1} (ma : Except ε α) (handle : εExcept ε α) :
Except ε α
Equations
def Except.orElseLazy {ε : Type u} {α : Type u_1} (x : Except ε α) (y : UnitExcept ε α) :
Except ε α
Equations
• = match x with | => | => y ()
@[always_inline]
instance Except.instMonadExcept {ε : Type u} :
Equations
def ExceptT (ε : Type u) (m : Type u → Type v) (α : Type u) :
Equations
@[inline]
def ExceptT.mk {ε : Type u} {m : Type u → Type v} {α : Type u} (x : m (Except ε α)) :
ExceptT ε m α
Equations
@[inline]
def ExceptT.run {ε : Type u} {m : Type u → Type v} {α : Type u} (x : ExceptT ε m α) :
m (Except ε α)
Equations
@[inline]
def ExceptT.pure {ε : Type u} {m : Type u → Type v} [inst : ] {α : Type u} (a : α) :
ExceptT ε m α
Equations
@[inline]
def ExceptT.bindCont {ε : Type u} {m : Type u → Type v} [inst : ] {α : Type u} {β : Type u} (f : αExceptT ε m β) :
Except ε αm (Except ε β)
Equations
• = match x with | => f a | => pure ()
@[inline]
def ExceptT.bind {ε : Type u} {m : Type u → Type v} [inst : ] {α : Type u} {β : Type u} (ma : ExceptT ε m α) (f : αExceptT ε m β) :
ExceptT ε m β
Equations
@[inline]
def ExceptT.map {ε : Type u} {m : Type u → Type v} [inst : ] {α : Type u} {β : Type u} (f : αβ) (x : ExceptT ε m α) :
ExceptT ε m β
Equations
@[inline]
def ExceptT.lift {ε : Type u} {m : Type u → Type v} [inst : ] {α : Type u} (t : m α) :
ExceptT ε m α
Equations
@[always_inline]
instance ExceptT.instMonadLiftExceptExceptT {ε : Type u} {m : Type u → Type v} [inst : ] :
Equations
• ExceptT.instMonadLiftExceptExceptT = { monadLift := fun {α} e => ExceptT.mk (pure e) }
instance ExceptT.instMonadLiftExceptT {ε : Type u} {m : Type u → Type v} [inst : ] :
Equations
@[inline]
def ExceptT.tryCatch {ε : Type u} {m : Type u → Type v} [inst : ] {α : Type u} (ma : ExceptT ε m α) (handle : εExceptT ε m α) :
ExceptT ε m α
Equations
instance ExceptT.instMonadFunctorExceptT {ε : Type u} {m : Type u → Type v} :
Equations
• ExceptT.instMonadFunctorExceptT = { monadMap := fun {α} f x => f (Except ε α) x }
@[always_inline]
instance ExceptT.instMonadExceptT {ε : Type u} {m : Type u → Type v} [inst : ] :
Equations
@[inline]
def ExceptT.adapt {ε : Type u} {m : Type u → Type v} [inst : ] {ε' : Type u} {α : Type u} (f : εε') :
ExceptT ε m αExceptT ε' m α
Equations
@[always_inline]
instance instMonadExceptOfExceptT (m : Type u → Type v) (ε₁ : Type u) (ε₂ : Type u) [inst : ] [inst : ] :
Equations
@[always_inline]
instance instMonadExceptOfExceptT_1 (m : Type u → Type v) (ε : Type u) [inst : ] :
Equations
• = { throw := fun {α} e => ExceptT.mk (pure ()), tryCatch := fun {α} => ExceptT.tryCatch }
instance instInhabitedExceptT {m : Type u_1 → Type u_2} {ε : Type u_1} {α : Type u_1} [inst : ] [inst : ] :
Inhabited (ExceptT ε m α)
Equations
• instInhabitedExceptT = { default := throw default }
instance instMonadExceptOfExcept (ε : Type u_1) :
Equations
• = { throw := fun {α} => Except.error, tryCatch := fun {α} => Except.tryCatch }
@[inline]
def MonadExcept.orelse' {ε : Type u} {m : Type v → Type w} [inst : ] {α : Type v} (t₁ : m α) (t₂ : m α) (useFirstEx : ) :
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.

Equations
@[inline]
def observing {ε : Type u} {α : Type u} {m : Type u → Type v} [inst : ] [inst : ] (x : m α) :
m (Except ε α)
Equations
def liftExcept {ε : Type u_1} {m : Type u_2 → Type u_3} {α : Type u_2} [inst : ] [inst : Pure m] :
Except ε αm α
Equations
• = match x with | => pure a | =>
instance instMonadControlExceptT (ε : Type u) (m : Type u → Type v) [inst : ] :
Equations
• = { stM := , liftWith := fun {α} f => liftM (f fun {β} x => ), restoreM := fun {α} x => x }
class MonadFinally (m : Type u → Type v) :
Type (max(u+1)v)
• tryFinally' x f runs x and then the "finally" computation f. When x succeeds with a : α, f (some a) is returned. If x fails for m's definition of failure, f none is returned. Hence tryFinally' can be thought of as performing the same role as a finally block in an imperative programming language.

tryFinally' : {α β : Type u} → m α(m β) → m (α × β)
Instances
@[inline]
def tryFinally {m : Type u → Type v} {α : Type u} {β : Type u} [inst : ] [inst : ] (x : m α) (finalizer : m β) :
m α

Execute x and then execute finalizer even if x threw an exception

Equations
@[always_inline]
instance Id.finally :
Equations
• Id.finally = { tryFinally' := fun {α β} x h => let a := x; let b := h (some x); pure (a, b) }
@[always_inline]
instance ExceptT.finally {m : Type u → Type v} {ε : Type u} [inst : ] [inst : ] :
Equations
• One or more equations did not get rendered due to their size.