inductive Lean.Exception : Type

Exception type used in most Lean monads

• error (ref : Syntax) (msg : MessageData) : Exception

  Error messages that are displayed to users. ref is used to provide position information.

• internal (id : InternalExceptionId) (extra : KVMap := { entries := [] }) : Exception

  Internal exceptions that are not meant to be seen by users. Examples: "postpone elaboration", "stuck at universe constraint", etc.

def Lean.Exception.toMessageData : Exception → MessageData

Convert exception into a structured message.

Equations

• (Lean.Exception.error ref msg).toMessageData = msg
• (Lean.Exception.internal id extra).toMessageData = (Lean.MessageData.ofFormat ∘ Std.format) id.toString

def Lean.Exception.hasSyntheticSorry : Exception → Bool

Equations

• (Lean.Exception.error ref msg).hasSyntheticSorry = msg.hasSyntheticSorry
• x✝.hasSyntheticSorry = false

def Lean.Exception.getRef : Exception → Syntax

Return syntax object providing position information for the exception. Recall that internal exceptions do not have position information.

Equations

• (Lean.Exception.error ref msg).getRef = ref
• (Lean.Exception.internal id extra).getRef = Lean.Syntax.missing

instance Lean.instInhabitedException : Inhabited Exception

Equations

• Lean.instInhabitedException = { default := Lean.Exception.error default default }

class Lean.AddErrorMessageContext (m : Type → Type) : Type

Similar to AddMessageContext, but for error messages. The default instance just uses AddMessageContext. In error messages, we may want to provide additional information (e.g., macro expansion stack), and refine the (ref : Syntax).

• add : Syntax → MessageData → m (Syntax × MessageData)

instance Lean.instAddErrorMessageContextOfAddMessageContextOfMonad (m : Type → Type) [AddMessageContext m] [Monad m] : AddErrorMessageContext m

Equations

• Lean.instAddErrorMessageContextOfAddMessageContextOfMonad m = { add := fun (ref : Lean.Syntax) (msg : Lean.MessageData) => do let msg ← Lean.addMessageContext msg pure (ref, msg) }

class Lean.MonadError (m : Type → Type) extends MonadExceptOf Lean.Exception m, Lean.MonadRef m, Lean.AddErrorMessageContext m : Type 1

• throw {α : Type} : Lean.Exception → m α
• tryCatch {α : Type} (body : m α) (handler : Lean.Exception → m α) : m α
• getRef : m Syntax
• withRef {α : Type} : Syntax → m α → m α
• add : Syntax → MessageData → m (Syntax × MessageData)

def Lean.throwError {m : Type → Type} {α : Type} [Monad m] [MonadError m] (msg : MessageData) : m α

Throw an error exception using the given message data. The result of getRef is used as position information. Recall that getRef returns the current "reference" syntax.

Equations

• Lean.throwError msg = do let ref ← Lean.getRef let __discr ← Lean.AddErrorMessageContext.add ref msg match __discr with | (ref, msg) => throw (Lean.Exception.error ref msg)

def Lean.throwUnknownConstant {m : Type → Type} {α : Type} [Monad m] [MonadError m] (constName : Name) : m α

Throw an unknown constant error message.

Equations

• Lean.throwUnknownConstant constName = Lean.throwError (Lean.toMessageData "unknown constant '" ++ Lean.toMessageData (Lean.MessageData.ofConstName constName) ++ Lean.toMessageData "'")

def Lean.throwErrorAt {m : Type → Type} {α : Type} [Monad m] [MonadError m] (ref : Syntax) (msg : MessageData) : m α

Throw an error exception using the given message data and reference syntax.

Equations

• Lean.throwErrorAt ref msg = Lean.withRef ref (Lean.throwError msg)

def Lean.ofExcept {m : Type → Type} {ε α : Type} [Monad m] [MonadError m] [ToMessageData ε] (x : Except ε α) : m α

Convert an Except into a m monadic action, where m is any monad that implements MonadError.

Equations

• Lean.ofExcept (Except.ok a) = pure a
• Lean.ofExcept (Except.error e) = Lean.throwError (Lean.toMessageData e)

opaque Lean.interruptExceptionId : InternalExceptionId

def Lean.throwInterruptException {m : Type → Type} {α : Type} [Monad m] [MonadError m] [MonadOptions m] : m α

Throws an internal interrupt exception that skips standard catch clauses and should be caught only at the top level of elaboration.

Equations

• Lean.throwInterruptException = throw (Lean.Exception.internal Lean.interruptExceptionId)

def Lean.Exception.isInterrupt : Exception → Bool

Returns true if the exception is an interrupt generated by checkInterrupted.

Equations

• (Lean.Exception.internal id extra).isInterrupt = (id == Lean.interruptExceptionId)
• x✝.isInterrupt = false

def Lean.throwKernelException {m : Type → Type} {α : Type} [Monad m] [MonadError m] [MonadOptions m] (ex : Kernel.Exception) : m α

Throw an error exception for the given kernel exception.

Equations

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

def Lean.ofExceptKernelException {m : Type → Type} {α : Type} [Monad m] [MonadError m] [MonadOptions m] (x : Except Kernel.Exception α) : m α

Lift from Except KernelException to m when m can throw kernel exceptions.

Equations

• Lean.ofExceptKernelException (Except.ok a) = pure a
• Lean.ofExceptKernelException (Except.error e) = Lean.throwKernelException e

class Lean.MonadRecDepth (m : Type → Type) : Type 1

• withRecDepth {α : Type} : Nat → m α → m α
• getRecDepth : m Nat
• getMaxRecDepth : m Nat

instance Lean.instMonadRecDepthReaderT {m : Type → Type} {ρ : Type} [MonadRecDepth m] : MonadRecDepth (ReaderT ρ m)

Equations

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

instance Lean.instMonadRecDepthStateRefT'OfMonad {m : Type → Type} {ω σ : Type} [Monad m] [MonadRecDepth m] : MonadRecDepth (StateRefT' ω σ m)

Equations

• Lean.instMonadRecDepthStateRefT'OfMonad = inferInstanceAs (Lean.MonadRecDepth (ReaderT (ST.Ref ω σ) m))

instance Lean.instMonadRecDepthMonadCacheTOfMonad {α : Type} {m : Type → Type} {ω β : Type} [BEq α] [Hashable α] [Monad m] [STWorld ω m] [MonadRecDepth m] : MonadRecDepth (MonadCacheT α β m)

Equations

• Lean.instMonadRecDepthMonadCacheTOfMonad = inferInstanceAs (Lean.MonadRecDepth (StateRefT' ω (Std.HashMap α β) m))

def Lean.throwMaxRecDepthAt {m : Type → Type} {α : Type} [MonadError m] (ref : Syntax) : m α

Throw a "maximum recursion depth has been reached" exception using the given reference syntax.

Equations

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

def Lean.Exception.isMaxRecDepth (ex : Exception) : Bool

Return true if ex was generated by throwMaxRecDepthAt. This function is a bit hackish. The max rec depth exception should probably be an internal exception, but it is also produced by MacroM which implemented in the prelude, and internal exceptions have not been defined yet.

Equations

• (Lean.Exception.error ref (Lean.MessageData.tagged `runtime.maxRecDepth a)).isMaxRecDepth = true
• ex.isMaxRecDepth = false

@[inline]

def Lean.withIncRecDepth {m : Type → Type} {α : Type} [Monad m] [MonadError m] [MonadRecDepth m] (x : m α) : m α

Increment the current recursion depth and then execute x. Throw an exception if maximum recursion depth has been reached. We use this combinator to prevent stack overflows.

Equations

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

def Lean.termThrowError__ : ParserDescr

Macro for throwing error exceptions. The argument can be an interpolated string. It is a convenient way of building MessageData objects. The result of getRef is used as position information. Recall that getRef returns the current "reference" syntax.

Equations

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

def Lean.termThrowErrorAt____ : ParserDescr

Macro for throwing error exceptions. The argument can be an interpolated string. It is a convenient way of building MessageData objects. The first argument must be a Syntax that provides position information for the error message. throwErrorAt ref msg is equivalent to withRef ref <| throwError msg

Equations

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