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

def Lean.ErrorExplanation.instFromJsonMetadata.fromJson : Json → Except String Metadata

Equations

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

instance Lean.ErrorExplanation.instFromJsonMetadata : FromJson Metadata

Equations

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

instance Lean.ErrorExplanation.instToJsonMetadata : ToJson Metadata

Equations

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

def Lean.ErrorExplanation.instToJsonMetadata.toJson : Metadata → Json

Equations

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

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

  The doc field is deprecated and should always be the empty 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

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] (name : Name) : m (Option ErrorExplanation)

Returns an error explanation for the given name if one exists.

Equations

• Lean.getErrorExplanation? name = do let __do_lift ← Lean.getEnv pure ((Lean.errorExplanationExt.getState __do_lift).find? name)

@[deprecated Lean.getErrorExplanation? (since := "2026-12-20")]

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

Equations

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

def Lean.hasErrorExplanation {m : Type → Type} [Monad m] [MonadEnv 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.getErrorExplanations {m : Type → Type} [Monad m] [MonadEnv m] : m (Array (Name × ErrorExplanation))

Returns all error explanations with their names, sorted by name.

Equations

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

@[deprecated Lean.getErrorExplanations (since := "2026-12-20")]

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

Equations

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

@[deprecated Lean.getErrorExplanations (since := "2026-12-20")]

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

Equations

• Lean.getErrorExplanationsSorted = Lean.getErrorExplanations