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

@[implicit_reducible]

instance Lean.ErrorExplanation.instFromJsonMetadata : FromJson Metadata

@[implicit_reducible]

instance Lean.ErrorExplanation.instToJsonMetadata : ToJson Metadata

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

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.

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.

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

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

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

Returns true if there exists an error explanation named 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.

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

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

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

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