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 := { })
: Exception
Internal exceptions that are not meant to be seen by users. Examples: "postpone elaboration", "stuck at universe constraint", etc.
Instances For
Convert exception into a structured message.
Equations
Instances For
Return syntax object providing position information for the exception. Recall that internal exceptions do not have position information.
Equations
Instances For
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)
Instances
Equations
- add : Syntax → MessageData → m (Syntax × MessageData)
Instances
Tag used for unknown identifier
messages.
This tag is used by the 'import unknown identifier' code action to detect messages that should
prompt the code action.
Equations
Instances For
Throw an error exception using the given message data and reference syntax.
Equations
Instances For
Creates a MessageData
that is tagged with unknownIdentifierMessageTag
.
This tag is used by the 'import unknown identifier' code action to detect messages that should
prompt the code action.
The end position of the range of an unknown identifier message should always point at the end of the
unknown identifier.
Equations
Instances For
Throw an unknown identifier error message that is tagged with unknownIdentifierMessageTag
.
The end position of the range of ref
should always point at the unknown identifier.
See also mkUnknownIdentifierMessage
.
Equations
Instances For
Throw an unknown constant error message.
The end position of the range of ref
should point at the unknown identifier.
See also mkUnknownIdentifierMessage
.
Equations
Instances For
Throw an unknown constant error message.
The end position of the range of the current reference should point at the unknown identifier.
See also mkUnknownIdentifierMessage
.
Equations
Instances For
Convert an Except
into a m
monadic action, where m
is any monad that
implements MonadError
.
Equations
Instances For
Throws an internal interrupt exception that skips standard catch
clauses and should be caught only
at the top level of elaboration.
Equations
Instances For
Returns true
if the exception is an interrupt generated by checkInterrupted
.
Equations
Instances For
Throw an error exception for the given kernel exception.
Equations
Instances For
Lift from Except KernelException
to m
when m
can throw kernel exceptions.
Equations
Instances For
Equations
Equations
Equations
Throw a "maximum recursion depth has been reached" exception using the given reference syntax.
Equations
Instances For
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
Instances For
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
Instances For
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