# Documentation

## Init.Control.Except

@[inline]
def Except.pure {ε : Type u} {α : Type u_1} (a : α) :
Except ε α
Equations
Instances For
@[inline]
def Except.map {ε : Type u} {α : Type u_1} {β : Type u_2} (f : αβ) :
Except ε αExcept ε β
Equations
Instances For
@[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
Instances For
@[inline]
def Except.bind {ε : Type u} {α : Type u_1} {β : Type u_2} (ma : Except ε α) (f : αExcept ε β) :
Except ε β
Equations
Instances For
@[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
Instances For
@[inline, reducible]
abbrev Except.isOk {ε : Type u} {α : Type u_1} :
Except ε αBool
Equations
• Except.isOk = Except.toBool
Instances For
@[inline]
def Except.toOption {ε : Type u} {α : Type u_1} :
Except ε α
Equations
• = match x with | => some a | => none
Instances For
@[inline]
def Except.tryCatch {ε : Type u} {α : Type u_1} (ma : Except ε α) (handle : εExcept ε α) :
Except ε α
Equations
Instances For
def Except.orElseLazy {ε : Type u} {α : Type u_1} (x : Except ε α) (y : UnitExcept ε α) :
Except ε α
Equations
• = match x with | => | => y ()
Instances For
@[always_inline]
instance Except.instMonadExcept {ε : Type u} :
Equations
def ExceptT (ε : Type u) (m : Type u → Type v) (α : Type u) :
Equations
Instances For
@[inline]
def ExceptT.mk {ε : Type u} {m : Type u → Type v} {α : Type u} (x : m (Except ε α)) :
ExceptT ε m α
Equations
Instances For
@[inline]
def ExceptT.run {ε : Type u} {m : Type u → Type v} {α : Type u} (x : ExceptT ε m α) :
m (Except ε α)
Equations
Instances For
@[inline]
def ExceptT.pure {ε : Type u} {m : Type u → Type v} [] {α : Type u} (a : α) :
ExceptT ε m α
Equations
Instances For
@[inline]
def ExceptT.bindCont {ε : Type u} {m : Type u → Type v} [] {α : Type u} {β : Type u} (f : αExceptT ε m β) :
Except ε αm (Except ε β)
Equations
• = match x with | => f a | => pure ()
Instances For
@[inline]
def ExceptT.bind {ε : Type u} {m : Type u → Type v} [] {α : Type u} {β : Type u} (ma : ExceptT ε m α) (f : αExceptT ε m β) :
ExceptT ε m β
Equations
Instances For
@[inline]
def ExceptT.map {ε : Type u} {m : Type u → Type v} [] {α : Type u} {β : Type u} (f : αβ) (x : ExceptT ε m α) :
ExceptT ε m β
Equations
Instances For
@[inline]
def ExceptT.lift {ε : Type u} {m : Type u → Type v} [] {α : Type u} (t : m α) :
ExceptT ε m α
Equations
Instances For
@[always_inline]
instance ExceptT.instMonadLiftExceptExceptT {ε : Type u} {m : Type u → Type v} [] :
Equations
instance ExceptT.instMonadLiftExceptT {ε : Type u} {m : Type u → Type v} [] :
Equations
• ExceptT.instMonadLiftExceptT = { monadLift := fun {α : Type u} => ExceptT.lift }
@[inline]
def ExceptT.tryCatch {ε : Type u} {m : Type u → Type v} [] {α : Type u} (ma : ExceptT ε m α) (handle : εExceptT ε m α) :
ExceptT ε m α
Equations
Instances For
instance ExceptT.instMonadFunctorExceptT {ε : Type u} {m : Type u → Type v} :
Equations
• ExceptT.instMonadFunctorExceptT = { monadMap := fun {α : Type u} (f : {β : Type u} → m βm β) (x : ExceptT ε m α) => f x }
@[always_inline]
instance ExceptT.instMonadExceptT {ε : Type u} {m : Type u → Type v} [] :
Equations
@[inline]
def ExceptT.adapt {ε : Type u} {m : Type u → Type v} [] {ε' : Type u} {α : Type u} (f : εε') :
ExceptT ε m αExceptT ε' m α
Equations
Instances For
@[always_inline]
instance instMonadExceptOfExceptT (m : Type u → Type v) (ε₁ : Type u) (ε₂ : Type u) [] [] :
Equations
• One or more equations did not get rendered due to their size.
@[always_inline]
instance instMonadExceptOfExceptT_1 (m : Type u → Type v) (ε : Type u) [] :
Equations
• = { throw := fun {α : Type u} (e : ε) => ExceptT.mk (pure ()), tryCatch := fun {α : Type u} => ExceptT.tryCatch }
instance instInhabitedExceptT {m : Type u_1 → Type u_2} {ε : Type u_1} {α : Type u_1} [] [] :
Inhabited (ExceptT ε m α)
Equations
• instInhabitedExceptT = { default := throw default }
instance instMonadExceptOfExcept (ε : Type u_1) :
Equations
• = { throw := fun {α : Type u_2} => Except.error, tryCatch := fun {α : Type u_2} => Except.tryCatch }
@[inline]
def MonadExcept.orelse' {ε : Type u} {m : Type v → Type w} [] {α : 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
Instances For
@[inline]
def observing {ε : Type u} {α : Type u} {m : Type u → Type v} [] [] (x : m α) :
m (Except ε α)
Equations
Instances For
def liftExcept {ε : Type u_1} {m : Type u_2 → Type u_3} {α : Type u_2} [] [Pure m] :
Except ε αm α
Equations
• = match x with | => pure a | =>
Instances For
instance instMonadControlExceptT (ε : Type u) (m : Type u → Type v) [] :
Equations
• One or more equations did not get rendered due to their size.
class MonadFinally (m : Type u → Type v) :
Type (max (u + 1) v)
• tryFinally' : {α β : Type u} → m α(m β)m (α × β)

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.

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

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

Equations
Instances For
@[always_inline]
instance Id.finally :
Equations
@[always_inline]
instance ExceptT.finally {m : Type u → Type v} {ε : Type u} [] [] :
Equations
• One or more equations did not get rendered due to their size.