structure Lean.ErrorExplanation.Metadata : Type

Metadata for an error explanation.

• summary gives a short description of the error
• sinceVersion indicates the version of Lean in which an error with this error name was introduced
• severity is the severity of the diagnostic
• removedVersion indicates the version of Lean in which this error name was retired, if applicable

• summary : String
• sinceVersion : String
• severity : MessageSeverity
• removedVersion? : Option String

instance Lean.ErrorExplanation.instFromJsonMetadata : FromJson Metadata

instance Lean.ErrorExplanation.instToJsonMetadata : ToJson Metadata

structure Lean.ErrorExplanation : Type

An explanation of a named error message.

Error explanations are rendered in the manual; a link to the resulting manual page is displayed at the bottom of corresponding error messages thrown using throwNamedError or throwNamedErrorAt.

• doc : String
• metadata : Metadata
• declLoc? : Option DeclarationLocation

def Lean.ErrorExplanation.summaryWithSeverity (explan : ErrorExplanation) : String

Returns the error explanation summary prepended with its severity. For use in completions and hovers.

inductive Lean.ErrorExplanation.CodeInfo.Kind : Type

The kind of a code block in an error explanation example. broken blocks raise the diagnostic being explained; fixed blocks must compile successfully.

• broken : Kind
• fixed : Kind

instance Lean.ErrorExplanation.CodeInfo.instReprKind : Repr Kind

instance Lean.ErrorExplanation.CodeInfo.instInhabitedKind : Inhabited Kind

instance Lean.ErrorExplanation.CodeInfo.instBEqKind : BEq Kind

instance Lean.ErrorExplanation.instToStringKind : ToString CodeInfo.Kind

def Lean.ErrorExplanation.CodeInfo.Kind.ofString : String → Option Kind

structure Lean.ErrorExplanation.CodeInfo : Type

Metadata about a code block in an error explanation, parsed from the block's info string.

• lang : String
• kind? : Option Kind
• title? : Option String

instance Lean.ErrorExplanation.instReprCodeInfo : Repr CodeInfo

def Lean.ErrorExplanation.CodeInfo.parse (s : String) : Except String CodeInfo

Parse metadata for an error explanation code block from its info string.

def Lean.ErrorExplanation.CodeInfo.parse.stringContents : Std.Internal.Parsec.String.Parser String

Parses the contents of a string literal up to, but excluding, the closing quotation mark.

def Lean.ErrorExplanation.CodeInfo.parse.upToWs (nonempty : Bool) : String.Iterator → Std.Internal.Parsec.ParseResult String String.Iterator

Parses all input up to the next whitespace. If nonempty is true, fails if there is no input prior to the next whitespace.

def Lean.ErrorExplanation.CodeInfo.parse.namedAttr : Std.Internal.Parsec.String.Parser (String × String)

Parses a named attribute, and returns its name and value.

def Lean.ErrorExplanation.CodeInfo.parse.attr : Std.Internal.Parsec.String.Parser (String ⊕ String × String)

Parses an "attribute" in an info string, either a space-delineated identifier or a named attribute of the form (name := "value").

def Lean.ErrorExplanation.CodeInfo.parse.infoString : Std.Internal.Parsec.String.Parser CodeInfo

instance Lean.ErrorExplanation.instReprValidationState : Repr Lean.ErrorExplanation.ValidationState✝

instance Lean.ErrorExplanation.instInhabitedValidationState : Inhabited Lean.ErrorExplanation.ValidationState✝

def Lean.ErrorExplanation.processDoc (doc : String) : Except (Nat × String) Unit

Validates that the given error explanation has the expected structure. If an error is found, it is represented as a pair (lineNumber, errorMessage) where lineNumber gives the 0-based offset from the first line of doc at which the error occurs.

opaque Lean.errorExplanationExt : SimplePersistentEnvExtension (Name × ErrorExplanation) (NameMap ErrorExplanation)

An environment extension that stores error explanations.

def Lean.getErrorExplanation? {m : Type → Type} [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] (name : Name) : m (Option ErrorExplanation)

Returns an error explanation for the given name if one exists, rewriting manual links.

def Lean.getErrorExplanationRaw? (env : Environment) (name : Name) : Option ErrorExplanation

Returns an error explanation for the given name if one exists without rewriting manual links.

In general, use Lean.getErrorExplanation? instead if the body of the explanation will be used.

def Lean.hasErrorExplanation {m : Type → Type} [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] (name : Name) : m Bool

Returns true if there exists an error explanation named name.

def Lean.getErrorExplanationsRaw (env : Environment) : Array (Name × ErrorExplanation)

Returns all error explanations with their names as an unsorted array, without rewriting manual links.

In general, use Lean.getErrorExplanations or Lean.getErrorExplanationsSorted instead of this function if the bodies of the fetched explanations will be used.

def Lean.getErrorExplanations {m : Type → Type} [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] : m (Array (Name × ErrorExplanation))

Returns all error explanations with their names, rewriting manual links.

def Lean.getErrorExplanationsSorted {m : Type → Type} [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] : m (Array (Name × ErrorExplanation))

Returns all error explanations with their names as a sorted array, rewriting manual links.