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

Equations

• Lean.ErrorExplanation.instFromJsonMetadata = { fromJson? := Lean.ErrorExplanation.fromJsonMetadata✝ }

instance Lean.ErrorExplanation.instToJsonMetadata : ToJson Metadata

Equations

• Lean.ErrorExplanation.instToJsonMetadata = { toJson := Lean.ErrorExplanation.toJsonMetadata✝ }

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.

Equations

• explan.summaryWithSeverity = toString "(" ++ toString explan.metadata.severity ++ toString ") " ++ toString explan.metadata.summary ++ toString ""

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

Equations

• Lean.ErrorExplanation.CodeInfo.instReprKind = { reprPrec := Lean.ErrorExplanation.CodeInfo.reprKind✝ }

instance Lean.ErrorExplanation.CodeInfo.instInhabitedKind : Inhabited Kind

Equations

• Lean.ErrorExplanation.CodeInfo.instInhabitedKind = { default := Lean.ErrorExplanation.CodeInfo.Kind.broken }

instance Lean.ErrorExplanation.CodeInfo.instBEqKind : BEq Kind

Equations

• Lean.ErrorExplanation.CodeInfo.instBEqKind = { beq := Lean.ErrorExplanation.CodeInfo.beqKind✝ }

instance Lean.ErrorExplanation.instToStringKind : ToString CodeInfo.Kind

Equations

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

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

Equations

• Lean.ErrorExplanation.CodeInfo.Kind.ofString "broken" = some Lean.ErrorExplanation.CodeInfo.Kind.broken
• Lean.ErrorExplanation.CodeInfo.Kind.ofString "fixed" = some Lean.ErrorExplanation.CodeInfo.Kind.fixed
• Lean.ErrorExplanation.CodeInfo.Kind.ofString x✝ = none

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

Equations

• Lean.ErrorExplanation.instReprCodeInfo = { reprPrec := Lean.ErrorExplanation.reprCodeInfo✝ }

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

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

Equations

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

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.

Equations

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

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.

Equations

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

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

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

Equations

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

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").

Equations

• Lean.ErrorExplanation.CodeInfo.parse.attr = (Sum.inr <$> Lean.ErrorExplanation.CodeInfo.parse.namedAttr <|> Sum.inl <$> Lean.ErrorExplanation.CodeInfo.parse.upToWs true)

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

Equations

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

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

Equations

• Lean.ErrorExplanation.instReprValidationState = { reprPrec := Lean.ErrorExplanation.reprValidationState✝ }

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

Equations

• Lean.ErrorExplanation.instInhabitedValidationState = { default := { lines := default, idx := default } }

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.

Equations

• Lean.ErrorExplanation.processDoc doc = Lean.ErrorExplanation.parseExplanation✝.run doc

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.

Equations

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

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.

Equations

• Lean.getErrorExplanationRaw? env name = (Lean.errorExplanationExt.getState env).find? name

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.

Equations

• Lean.hasErrorExplanation name = do let __do_lift ← Lean.getEnv pure ((Lean.errorExplanationExt.getState __do_lift).contains 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.

Equations

• Lean.getErrorExplanationsRaw env = Lean.RBMap.toArray (Lean.errorExplanationExt.getState env)

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.

Equations

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

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.

Equations

• Lean.getErrorExplanationsSorted = do let __do_lift ← Lean.getErrorExplanations pure (__do_lift.qsort fun (e e' : Lean.Name × Lean.ErrorExplanation) => decide (e.fst.toString < e'.fst.toString))