@[inline]

def Except.pure {ε : Type u} {α : Type u_1} (a : α) : Except ε α

A successful computation in the Except ε monad: a is returned, and no exception is thrown.

@[inline]

def Except.map {ε : Type u} {α : Type u_1} {β : Type u_2} (f : α → β) : Except ε α → Except ε β

Transforms a successful result with a function, doing nothing when an exception is thrown.

Examples:

• (pure 2 : Except String Nat).map toString = pure 2
• (throw "Error" : Except String Nat).map toString = throw "Error"

@[simp]

theorem Except.map_id {ε : Type u} {α : Type u_1} : Except.map id = id

@[inline]

def Except.mapError {ε : Type u} {ε' : Type u_1} {α : Type u_2} (f : ε → ε') : Except ε α → Except ε' α

Transforms exceptions with a function, doing nothing on successful results.

Examples:

• (pure 2 : Except String Nat).mapError (·.length) = pure 2
• (throw "Error" : Except String Nat).mapError (·.length) = throw 5

@[inline]

def Except.bind {ε : Type u} {α : Type u_1} {β : Type u_2} (ma : Except ε α) (f : α → Except ε β) : Except ε β

Sequences two operations that may throw exceptions, allowing the second to depend on the value returned by the first.

If the first operation throws an exception, then it is the result of the computation. If the first succeeds but the second throws an exception, then that exception is the result. If both succeed, then the result is the result of the second computation.

This is the implementation of the >>= operator for Except ε.

@[inline]

def Except.toBool {ε : Type u} {α : Type u_1} : Except ε α → Bool

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

@[reducible, inline]

abbrev Except.isOk {ε : Type u} {α : Type u_1} : Except ε α → Bool

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

@[inline]

def Except.toOption {ε : Type u} {α : Type u_1} : Except ε α → Option α

Returns none if an exception was thrown, or some around the value on success.

Examples:

• (pure 10 : Except String Nat).toOption = some 10
• (throw "Failure" : Except String Nat).toOption = none

@[inline]

def Except.tryCatch {ε : Type u} {α : Type u_1} (ma : Except ε α) (handle : ε → Except ε α) : Except ε α

Handles exceptions thrown in the Except ε monad.

If ma is successful, its result is returned. If it throws an exception, then handle is invoked on the exception's value.

Examples:

• (pure 2 : Except String Nat).tryCatch (pure ·.length) = pure 2
• (throw "Error" : Except String Nat).tryCatch (pure ·.length) = pure 5
• (throw "Error" : Except String Nat).tryCatch (fun x => throw ("E: " ++ x)) = throw "E: Error"

def Except.orElseLazy {ε : Type u} {α : Type u_1} (x : Except ε α) (y : Unit → Except ε α) : Except ε α

Recovers from exceptions thrown in the Except ε monad. Typically used via the <|> operator.

Except.tryCatch is a related operator that allows the recovery procedure to depend on which exception was thrown.

@[implicit_reducible, always_inline]

instance Except.instMonad {ε : Type u} : Monad (Except ε)

def ExceptT (ε : Type u) (m : Type u → Type v) (α : Type u) : Type v

Adds exceptions of type ε to a monad m.

@[inline]

def ExceptT.mk {ε : Type u} {m : Type u → Type v} {α : Type u} (x : m (Except ε α)) : ExceptT ε m α

Use a monadic action that may return an exception's value as an action in the transformed monad that may throw the corresponding exception.

This is the inverse of ExceptT.run.

@[inline]

def ExceptT.run {ε : Type u} {m : Type u → Type v} {α : Type u} (x : ExceptT ε m α) : m (Except ε α)

Use a monadic action that may throw an exception as an action that may return an exception's value.

This is the inverse of ExceptT.mk.

@[inline]

def ExceptT.runK {m : Type u_1 → Type u_2} {ε α β : Type u_1} [Monad m] (x : ExceptT ε m α) (ok : α → m β) (error : ε → m β) : m β

Use a monadic action that may throw an exception by providing explicit success and failure continuations.

@[inline]

def ExceptT.runCatch {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] (x : ExceptT α m α) : m α

Returns the value of a computation, forgetting whether it was an exception or a success.

This corresponds to early return.

@[inline]

def ExceptT.pure {ε : Type u} {m : Type u → Type v} [Monad m] {α : Type u} (a : α) : ExceptT ε m α

Returns the value a without throwing exceptions or having any other effect.

@[inline]

def ExceptT.bindCont {ε : Type u} {m : Type u → Type v} [Monad m] {α β : Type u} (f : α → ExceptT ε m β) : Except ε α → m (Except ε β)

Handles exceptions thrown by an action that can have no effects other than throwing exceptions.

@[inline]

def ExceptT.bind {ε : Type u} {m : Type u → Type v} [Monad m] {α β : Type u} (ma : ExceptT ε m α) (f : α → ExceptT ε m β) : ExceptT ε m β

Sequences two actions that may throw exceptions. Typically used via do-notation or the >>= operator.

@[inline]

def ExceptT.map {ε : Type u} {m : Type u → Type v} [Monad m] {α β : Type u} (f : α → β) (x : ExceptT ε m α) : ExceptT ε m β

Transforms a successful computation's value using f. Typically used via the <$> operator.

@[inline]

def ExceptT.lift {ε : Type u} {m : Type u → Type v} [Monad m] {α : Type u} (t : m α) : ExceptT ε m α

Runs a computation from an underlying monad in the transformed monad with exceptions.

@[implicit_reducible, always_inline]

instance ExceptT.instMonadLiftExcept {ε : Type u} {m : Type u → Type v} [Monad m] : MonadLift (Except ε) (ExceptT ε m)

@[implicit_reducible]

instance ExceptT.instMonadLift {ε : Type u} {m : Type u → Type v} [Monad m] : MonadLift m (ExceptT ε m)

@[inline]

def ExceptT.tryCatch {ε : Type u} {m : Type u → Type v} [Monad m] {α : Type u} (ma : ExceptT ε m α) (handle : ε → ExceptT ε m α) : ExceptT ε m α

Handles exceptions produced in the ExceptT ε transformer.

@[implicit_reducible]

instance ExceptT.instMonadFunctor {ε : Type u} {m : Type u → Type v} : MonadFunctor m (ExceptT ε m)

@[implicit_reducible, always_inline]

instance ExceptT.instMonad {ε : Type u} {m : Type u → Type v} [Monad m] : Monad (ExceptT ε m)

@[inline]

def ExceptT.adapt {ε : Type u} {m : Type u → Type v} [Monad m] {ε' α : Type u} (f : ε → ε') : ExceptT ε m α → ExceptT ε' m α

Transforms exceptions using the function f.

This is the ExceptT version of Except.mapError.

@[implicit_reducible, always_inline]

instance instMonadExceptOfExceptT (m : Type u → Type v) (ε₁ ε₂ : Type u) [MonadExceptOf ε₁ m] : MonadExceptOf ε₁ (ExceptT ε₂ m)

@[implicit_reducible, always_inline]

instance instMonadExceptOfExceptTOfMonad (m : Type u → Type v) (ε : Type u) [Monad m] : MonadExceptOf ε (ExceptT ε m)

@[implicit_reducible]

instance instInhabitedExceptTOfMonad {m : Type u_1 → Type u_2} {ε α : Type u_1} [Monad m] [Inhabited ε] : Inhabited (ExceptT ε m α)

@[implicit_reducible]

instance instMonadExceptOfExcept (ε : Type u_1) : MonadExceptOf ε (Except ε)

@[inline]

def MonadExcept.orelse' {ε : Type u} {m : Type v → Type w} [MonadExcept ε m] {α : Type v} (t₁ t₂ : m α) (useFirstEx : Bool := true) : m α

An alternative unconditional error recovery operator that allows callers to specify which exception to throw in cases where both operations throw exceptions.

By default, the first is thrown, because the <|> operator throws the second.

@[inline]

def observing {ε α : Type u} {m : Type u → Type v} [Monad m] [MonadExcept ε m] (x : m α) : m (Except ε α)

def liftExcept {ε : Type u_1} {m : Type u_2 → Type u_3} {α : Type u_2} [MonadExceptOf ε m] [Pure m] : Except ε α → m α

@[implicit_reducible]

instance instMonadControlExceptTOfMonad (ε : Type u) (m : Type u → Type v) [Monad m] : MonadControl m (ExceptT ε m)

class MonadFinally (m : Type u → Type v) : Type (max (u + 1) v)

Monads that provide the ability to ensure an action happens, regardless of exceptions or other failures.

MonadFinally.tryFinally' is used to desugar try ... finally ... syntax.

• tryFinally' {α β : Type u} (x : m α) (f : Option α → m β) : m (α × β)

  Runs an action, ensuring that some other action always happens afterward.

  More specifically, tryFinally' x f runs x and then the “finally” computation f. If x succeeds with some value a : α, f (some a) is returned. If x fails for m's definition of failure, f none is returned.

  tryFinally' can be thought of as performing the same role as a finally block in an imperative programming language.

@[inline]

def tryFinally {m : Type u → Type v} {α β : Type u} [MonadFinally m] [Functor m] (x : m α) (finalizer : m β) : m α

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

@[implicit_reducible, always_inline]

instance Id.finally : MonadFinally Id

@[implicit_reducible, always_inline]

instance ExceptT.finally {m : Type u → Type v} {ε : Type u} [MonadFinally m] [Monad m] : MonadFinally (ExceptT ε m)

@[implicit_reducible]

instance instMonadAttachExceptTOfMonad {m : Type (max u_1 u_2) → Type u_3} {ε : Type (max u_1 u_2)} [Monad m] [MonadAttach m] : MonadAttach (ExceptT ε m)