@[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.

Equations

• Except.pure a = Except.ok a

@[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"

Equations

• Except.map f (Except.error err) = Except.error err
• Except.map f (Except.ok v) = Except.ok (f v)

@[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

Equations

• Except.mapError f (Except.error err) = Except.error (f err)
• Except.mapError f (Except.ok v) = Except.ok v

@[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 ε.

Equations

• (Except.error err).bind f = Except.error err
• (Except.ok v).bind f = f v

@[inline]

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

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

Equations

• (Except.ok a).toBool = true
• (Except.error a).toBool = false

@[reducible, inline]

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

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

Equations

• Except.isOk = Except.toBool

@[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

Equations

• (Except.ok a).toOption = some a
• (Except.error a).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"

Equations

• (Except.ok a).tryCatch handle = Except.ok a
• (Except.error a).tryCatch handle = handle a

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.

Equations

• (Except.ok a).orElseLazy y = Except.ok a
• (Except.error a).orElseLazy y = y ()

@[always_inline]

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

Equations

• One or more equations did not get rendered due to their size.

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

Adds exceptions of type ε to a monad m.

Equations

• ExceptT ε m α = m (Except ε α)

Instances For

• ExceptT.finally
• ExceptT.instLawfulMonad
• ExceptT.instMonad
• ExceptT.instMonadFunctor
• ExceptT.instMonadLift
• ExceptT.instMonadLiftExcept
• Lake.instMonadLiftTExceptTOfMonadOfMonadExceptOf_lake
• Lean.Order.instCCPOExceptTOfMonadOfPartialOrder
• Lean.Order.instMonoBindExceptTOfCCPO
• Lean.Order.instPartialOrderExceptTOfMonad
• Lean.instMonadBacktrackExceptTOfMonad
• Lean.instMonadCacheExceptTOfMonad
• instInhabitedExceptTOfMonad
• instMonadControlExceptTOfMonad
• instMonadExceptOfExceptT
• instMonadExceptOfExceptTOfMonad

@[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.

Equations

• ExceptT.mk x = x

@[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.

Equations

• x.run = x

@[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.

Equations

• ExceptT.pure a = ExceptT.mk (pure (Except.ok a))

@[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.

Equations

• ExceptT.bindCont f (Except.ok a) = f a
• ExceptT.bindCont f (Except.error e) = pure (Except.error e)

@[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.

Equations

• ma.bind f = ExceptT.mk (ma >>= ExceptT.bindCont f)

@[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.

Equations

• ExceptT.map f x = ExceptT.mk do let a ← x match a with | Except.ok a => pure (Except.ok (f a)) | Except.error e => pure (Except.error e)

@[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.

Equations

• ExceptT.lift t = ExceptT.mk (Except.ok <$> t)

@[always_inline]

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

Equations

• ExceptT.instMonadLiftExcept = { monadLift := fun {α : Type ?u.20} (e : Except ε α) => ExceptT.mk (pure e) }

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

Equations

• ExceptT.instMonadLift = { monadLift := fun {α : Type ?u.18} => ExceptT.lift }

@[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.

Equations

• ma.tryCatch handle = ExceptT.mk do let res ← ma match res with | Except.ok a => pure (Except.ok a) | Except.error e => handle e

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

Equations

• ExceptT.instMonadFunctor = { monadMap := fun {α : Type ?u.18} (f : {β : Type ?u.18} → m β → m β) (x : ExceptT ε m α) => f x }

@[always_inline]

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

Equations

• One or more equations did not get rendered due to their size.

@[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.

Equations

• ExceptT.adapt f x = ExceptT.mk (Except.mapError f <$> x)

@[always_inline]

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

Equations

• One or more equations did not get rendered due to their size.

@[always_inline]

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

Equations

• instMonadExceptOfExceptTOfMonad m ε = { throw := fun {α : Type ?u.20} (e : ε) => ExceptT.mk (pure (Except.error e)), tryCatch := fun {α : Type ?u.20} => ExceptT.tryCatch }

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

Equations

• instInhabitedExceptTOfMonad = { default := throw default }

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

Equations

• instMonadExceptOfExcept ε = { throw := fun {α : Type ?u.9} => Except.error, tryCatch := fun {α : Type ?u.9} => Except.tryCatch }

@[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.

Equations

• MonadExcept.orelse' t₁ t₂ useFirstEx = tryCatch t₁ fun (e₁ : ε) => tryCatch t₂ fun (e₂ : ε) => throw (if useFirstEx = true then e₁ else e₂)

@[inline]

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

Equations

• observing x = tryCatch (do let a ← x pure (Except.ok a)) fun (ex : ε) => pure (Except.error ex)

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

Equations

• liftExcept (Except.ok a) = pure a
• liftExcept (Except.error a) = throw a

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

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)

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.

Instances

• EStateM.instMonadFinally
• ExceptT.finally
• Id.finally
• Lake.EStateT.instMonadFinallyOfMonad
• Lake.EquipT.instMonadFinallyOfMonad
• Lean.MonadCacheT.instMonadFinally
• Lean.MonadStateCacheT.instMonadFinally
• ReaderT.tryFinally
• StateT.tryFinally
• instMonadFinallyBaseIO
• instMonadFinallyEIO
• instMonadFinallyStateRefT'

@[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

Equations

• tryFinally x finalizer = (fun (x : α × β) => x.fst) <$> tryFinally' x fun (x : Option α) => finalizer

@[always_inline]

instance Id.finally : MonadFinally Id

Equations

• Id.finally = { tryFinally' := fun {α β : Type ?u.10} (x : Id α) (h : Option α → Id β) => let a := x; let b := h (some x); pure (a, b) }

@[always_inline]

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

Equations

• One or more equations did not get rendered due to their size.