stop using deprecated functions

src/Lean.lean

@@ -44,7 +44,6 @@ public import Lean.LibrarySuggestions
 public import Lean.Namespace
 public import Lean.EnvExtension
 public import Lean.ErrorExplanation
-public import Lean.ErrorExplanations
 public import Lean.DefEqAttrib
 public import Lean.Shell
 public import Lean.ExtraModUses

src/Lean/Elab/ErrorExplanation.lean

@@ -84,19 +84,19 @@ def elabCheckedNamedError : TermElab := fun stx expType? => do
   addCompletionInfo <| CompletionInfo.errorName span partialId
   let name := id.getId.eraseMacroScopes
   pushInfoLeaf <| .ofErrorNameInfo { stx := id, errorName := name }
-  if let some explan := getErrorExplanationRaw? (← getEnv) name then
+  if let some explan ← getErrorExplanation? name then
     if let some removedVersion := explan.metadata.removedVersion? then
       logWarningAt id m!"The error name `{name}` was removed in Lean version {removedVersion} and \
         should not be used."
   else
-    logErrorAt id m!"There is no explanation associated with the name `{name}`. \
-      Add an explanation of this error to the `Lean.ErrorExplanations` module."
+    logErrorAt id m!"There is no explanation registered with the name `{name}`. \
+      Register an explanation for this error in the `Lean.ErrorExplanation` module."
   let stx' ← liftMacroM <| expandNamedErrorMacro stx
   elabTerm stx' expType?
 
 open Command in
 @[builtin_command_elab registerErrorExplanationStx] def elabRegisterErrorExplanation : CommandElab
-| `(registerErrorExplanationStx| $docStx:docComment register_error_explanation%$cmd $id:ident $t:term) => withRef cmd do
+| `(registerErrorExplanationStx| $_docStx register_error_explanation%$cmd $id:ident $t:term) => withRef cmd do
   unless (← getEnv).contains ``ErrorExplanation.Metadata do
     throwError "To use this command, add `import Lean.ErrorExplanation` to the header of this file"
   recordExtraModUseFromDecl ``ErrorExplanation.Metadata (isMeta := true)
@@ -116,18 +116,8 @@ open Command in
     throwErrorAt id m!"Invalid name `{name}`: Error explanation names must have two components"
       ++ .note m!"The first component of an error explanation name identifies the package from \
         which the error originates, and the second identifies the error itself."
-  runTermElabM fun _ => validateDocComment docStx
-  let doc ← getDocStringText docStx
   if errorExplanationExt.getState (← getEnv) |>.contains name then
     throwErrorAt id m!"Cannot add explanation: An error explanation already exists for `{name}`"
-  if let .error (lineOffset, msg) := ErrorExplanation.processDoc doc then
-    let some range := docStx.raw[1].getRange? | throwError msg
-    let fileMap ← getFileMap
-    let ⟨startLine, _⟩ := fileMap.toPosition range.start
-    let errLine := startLine + lineOffset
-    let synth := Syntax.ofRange { start := fileMap.ofPosition ⟨errLine, 0⟩,
-                                  stop  := fileMap.ofPosition ⟨errLine + 1, 0⟩ }
-    throwErrorAt synth msg
   let (declLoc? : Option DeclarationLocation) ← do
     let map ← getFileMap
     let start := id.raw.getPos?.getD 0
@@ -136,5 +126,5 @@ open Command in
       module := (← getMainModule)
       range := .ofStringPositions map start fin
     }
-  modifyEnv (errorExplanationExt.addEntry · (name, { metadata, doc, declLoc? }))
+  modifyEnv (errorExplanationExt.addEntry · (name, { doc := "", metadata, declLoc? }))
 | _ => throwUnsupportedSyntax

src/Lean/Elab/Tactic/Induction.lean

@@ -12,7 +12,6 @@ public import Lean.Elab.Tactic.ElabTerm
 import Lean.Meta.Tactic.FunIndCollect
 import Lean.Elab.App
 import Lean.Elab.Tactic.Generalize
-import Lean.ErrorExplanations.InductionWithNoAlts
 
 
 public section

src/Lean/ErrorExplanation.lean

@@ -40,288 +40,18 @@ Error explanations are rendered in the manual; a link to the resulting manual pa
 the bottom of corresponding error messages thrown using `throwNamedError` or `throwNamedErrorAt`.
 -/
 structure ErrorExplanation where
+  /-- The `doc` field is deprecated and should always be the empty string -/
   doc : String
   metadata : ErrorExplanation.Metadata
   declLoc? : Option DeclarationLocation
 
-namespace ErrorExplanation
-
 /--
 Returns the error explanation summary prepended with its severity. For use in completions and
 hovers.
 -/
-def summaryWithSeverity (explan : ErrorExplanation) : String :=
+def ErrorExplanation.summaryWithSeverity (explan : ErrorExplanation) : String :=
   s!"({explan.metadata.severity}) {explan.metadata.summary}"
 
-/--
-The kind of a code block in an error explanation example. `broken` blocks raise the diagnostic being
-explained; `fixed` blocks must compile successfully.
--/
-inductive CodeInfo.Kind
-  | broken | fixed
-  deriving Repr, Inhabited, BEq
-
-instance : ToString CodeInfo.Kind where
-  toString
-  | .broken => "broken"
-  | .fixed => "fixed"
-
-def CodeInfo.Kind.ofString : String → Option CodeInfo.Kind
-  | "broken" => some .broken
-  | "fixed" => some .fixed
-  | _ => none
-
-/-- Metadata about a code block in an error explanation, parsed from the block's info string. -/
-structure CodeInfo where
-  lang : String
-  kind? : Option CodeInfo.Kind
-  title? : Option String
-deriving Repr
-
-open Std.Internal Parsec Parsec.String in
-/-- Parse metadata for an error explanation code block from its info string. -/
-def CodeInfo.parse (s : String) : Except String CodeInfo :=
-  infoString.run s |>.mapError (fun e => s!"Invalid code block info string `{s}`: {e}")
-where
-  /-- Parses the contents of a string literal up to, but excluding, the closing quotation mark. -/
-  stringContents : Parser String := attempt do
-    let escaped := pchar '\\' *> pchar '"'
-    let cs ← many (notFollowedBy (pchar '"') *> (escaped <|> any))
-    return String.ofList cs.toList
-
-  /--
-  Parses all input up to the next whitespace. If `nonempty` is `true`, fails if there is no input
-  prior to the next whitespace.
-  -/
-  upToWs (nonempty : Bool) : Parser String := fun it =>
-    let it' := (it.2.find? fun (c : Char) => c.isWhitespace).getD it.1.endPos
-    if nonempty && it' == it.2 then
-      .error ⟨_, it'⟩ (.other "Expected a nonempty string")
-    else
-      .success ⟨_, it'⟩ (it.1.slice! it.2 it').copy
-
-  /-- Parses a named attribute, and returns its name and value. -/
-  namedAttr : Parser (String × String) := attempt do
-    let name ← skipChar '(' *> ws *> (upToWs true)
-    let contents ← ws *> skipString ":=" *> ws *> skipChar '"' *> stringContents
-    discard <| skipChar '"' *> ws *> skipChar ')'
-    return (name, contents)
-
-  /--
-  Parses an "attribute" in an info string, either a space-delineated identifier or a named
-  attribute of the form `(name := "value")`.
-  -/
-  attr : Parser (String ⊕ String × String) :=
-    .inr <$> namedAttr <|> .inl <$> (upToWs true)
-
-  infoString : Parser CodeInfo := do
-    let lang ← upToWs false
-    let attrs ← many (attempt <| ws *> attr)
-    let mut kind? := Option.none
-    let mut title? := Option.none
-    for attr in attrs do
-      match attr with
-      | .inl atomicAttr =>
-        match atomicAttr with
-        | "broken" | "fixed" =>
-          match kind? with
-          | none => kind? := Kind.ofString atomicAttr
-          | some kind =>
-            fail s!"Redundant kind specifications: previously `{kind}`; now `{atomicAttr}`"
-        | _ => fail s!"Invalid attribute `{atomicAttr}`"
-      | .inr (name, val) =>
-        if name == "title" then
-          if title?.isNone then
-            title? := some val
-          else
-            fail "Redundant title specifications"
-        else
-          fail s!"Invalid named attribute `{name}`; expected `title`"
-    return { lang, title?, kind? }
-
-open Std.Internal Parsec
-
-/--
-An iterator storing nonempty lines in an error explanation together with their original line
-numbers.
--/
-private structure ValidationState where
-  lines : Array (String × Nat)
-  idx   : Nat := 0
-deriving Repr, Inhabited
-
-/-- Creates an iterator for validation from the raw contents of an error explanation. -/
-private def ValidationState.ofSource (input : String) : ValidationState where
-  lines := input.split '\n'
-    |>.filter (!·.trimAscii.isEmpty)
-    |>.toStringArray
-    |>.zipIdx
-
--- Workaround to account for the fact that `Input` expects "EOF" to be a valid position
-private def ValidationState.get (s : ValidationState) :=
-  if _ : s.idx < s.lines.size then
-    s.lines[s.idx].1
-  else
-    ""
-
-private def ValidationState.getLineNumber (s : ValidationState) :=
-  if _ : s.lines.size = 0 then
-    0
-  else
-    s.lines[min s.idx (s.lines.size - 1)].2
-
-private instance : Input ValidationState String Nat where
-  pos := ValidationState.idx
-  next := fun s => { s with idx := min (s.idx + 1) s.lines.size }
-  curr := ValidationState.get
-  hasNext := fun s => s.idx < s.lines.size
-  next' := fun s _ => { s with idx := s.idx + 1 }
-  curr' := fun s _ => s.get
-
-private abbrev ValidationM := Parsec ValidationState
-
-private def ValidationM.run (p : ValidationM α) (input : String) : Except (Nat × String) α :=
-  match p (.ofSource input) with
-  | .success _ res => Except.ok res
-  | .error s err  => Except.error (s.getLineNumber, toString err)
-
-/--
-Matches `p` as many times as possible, followed by EOF. If `p` cannot be matched prior to the end
-of the input, rethrows the corresponding error.
--/
-private partial def manyThenEOF (p : ValidationM α) : ValidationM Unit := fun s =>
-  match eof s with
-  | .success .. => .success s ()
-  | .error .. =>
-    match p s with
-    | .success s' _ => manyThenEOF p s'
-    | .error s' err => .error s' err
-
-/-- Repeatedly parses the next input as long as it satisfies `p`, and discards the result. -/
-private partial def manyD (p : ValidationM α) : ValidationM Unit :=
-  Parsec.tryCatch p (fun _ => manyD p) (fun _ => pure ())
-
-/-- Parses one or more inputs as long as they satisfy `p`, and discards the result. -/
-private def many1D (p : ValidationM α) : ValidationM Unit :=
-  p *> manyD p
-
-/-- Repeatedly parses the next input as long as it fails to satisfy `p`, and discards the result. -/
-private def manyNotD (p : ValidationM α) : ValidationM Unit :=
-  manyD (notFollowedBy p *> skip)
-
-/-- Parses an error explanation: a general description followed by an examples section. -/
-private def parseExplanation : ValidationM Unit := do
-  manyNotD examplesHeader
-  eof <|> (examplesHeader *> manyThenEOF singleExample)
-where
-  /-- The top-level `# Examples` header -/
-  examplesHeader := attempt do
-    let line ← any
-    if (matchHeader 1 "Examples" line).isSome then
-      return
-    else
-      fail s!"Expected level-1 'Examples' header, but found `{line}`"
-
-  -- We needn't `attempt` examples because they never appear in a location where backtracking is
-  -- possible, and persisting the line index allows better error message placement
-  singleExample := do
-    let header ← exampleHeader
-    labelingExampleErrors header do
-      codeBlock "lean" (some .broken)
-      many1D (codeBlock "output")
-      many1D do
-        let leanBlock ← codeBlock "lean" (some .fixed)
-        let outputBlocks ← many (codeBlock "output")
-        return (leanBlock, outputBlocks)
-      manyNotD exampleEndingHeader
-
-  /-- A level-2 header for a single example. -/
-  exampleHeader := attempt do
-    let line ← any
-    if let some header := matchHeader 2 none line then
-      return header
-    else
-      fail s!"Expected level-2 header for an example section, but found `{line}`"
-
-  /-- A header capable of ending an example. -/
-  exampleEndingHeader := attempt do
-    let line ← any
-    if (matchHeader 1 none line).isSome || (matchHeader 2 none line).isSome then
-      return
-    else
-      fail s!"Expected a level-1 or level-2 header, but found `{line}`"
-
-  codeBlock (lang : String) (kind? : Option ErrorExplanation.CodeInfo.Kind := none) := attempt do
-    let (numTicks, infoString) ← fence
-      <|> fail s!"Expected a(n){kind?.map (s!" {·}") |>.getD ""} `{lang}` code block"
-    manyD (notFollowedBy (fence numTicks) *> any)
-    let (_, closing) ← fence numTicks
-      <|> fail s!"Missing closing code fence for block with header '{infoString}'"
-    -- Validate code block:
-    unless closing.trimAscii.isEmpty do
-      fail s!"Expected a closing code fence, but found the nonempty info string `{closing}`"
-    let info ← match ErrorExplanation.CodeInfo.parse infoString.copy with
-      | .ok i => pure i
-      | .error s =>
-        fail s
-    let langMatches := info.lang == lang
-    let kindMatches := (kind?.map (some · == info.kind?)).getD true
-    unless langMatches && kindMatches do
-      let (expKind, actKind) := match kind? with
-        | some kind =>
-          let actualKindStr := (info.kind?.map (s!" {·}")).getD " unspecified-kind"
-          (s!" {kind}", actualKindStr)
-        | none => ("", "")
-      fail s!"Expected a(n){expKind} `{lang}` code block, but found a(n){actKind} `{info.lang}` one"
-
-  fence (ticksToClose : Option Nat := none) := attempt do
-    let line ← any
-    if line.startsWith "```" then
-      let numTicks := line.takeWhile (· == '`') |>.utf8ByteSize -- this makes sense because we know the slice consists only of ticks
-      match ticksToClose with
-      | none => return (numTicks, line.drop numTicks)
-      | some n =>
-        if numTicks == n then
-          return (numTicks, line.drop numTicks)
-        else
-          fail s!"Expected a closing code fence with {n} ticks, but found:\n{line}"
-    else
-      -- Don't put `line` in backticks here because it might be a partial code fence
-      fail s!"Expected a code fence, but found:\n{line}"
-
-  /-- Prepends an error raised by `x` to indicate that it arose in example `header`. -/
-  labelingExampleErrors {α} (header : String) (x : ValidationM α) : ValidationM α := fun s =>
-    match x s with
-    | res@(.success ..) => res
-    | .error s' msg => .error s' (.other s!"Example '{header}' is malformed: {msg}")
-
-  /--
-  If `line` is a level-`level` header and, if `title?` is non-`none`, its title is `title?`,
-  then returns the contents of the header at `line` (i.e., stripping the leading `#`). Returns
-  `none` if `line` is not a header of the appropriate form.
-  -/
-  matchHeader (level : Nat) (title? : Option String) (line : String) : Option String := do
-    let octsEndPos := String.Pos.Raw.nextWhile line (· == '#') 0
-    guard (octsEndPos.byteIdx == level)
-    guard (octsEndPos.get line == ' ')
-    let titleStartPos := octsEndPos.next line
-    let title := Substring.Raw.mk line titleStartPos line.rawEndPos |>.toString
-    let titleMatches : Bool := match title? with
-      | some expectedTitle => title == expectedTitle
-      | none => true
-    guard titleMatches
-    some title
-
-/--
-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.
--/
-def processDoc (doc : String) : Except (Nat × String) Unit :=
-  parseExplanation.run doc
-
-end ErrorExplanation
-
 /-- An environment extension that stores error explanations.  -/
 builtin_initialize errorExplanationExt : SimplePersistentEnvExtension (Name × ErrorExplanation) (NameMap ErrorExplanation) ←
   registerSimplePersistentEnvExtension {
@@ -332,44 +62,126 @@ builtin_initialize errorExplanationExt : SimplePersistentEnvExtension (Name × E
           acc.insert n v
   }
 
-/-- Returns an error explanation for the given name if one exists, rewriting manual links. -/
-def getErrorExplanation? [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] (name : Name) : m (Option ErrorExplanation) := do
-  let explan? := errorExplanationExt.getState (← getEnv) |>.find? name
-  explan?.mapM fun explan =>
-    return { explan with doc := (← rewriteManualLinks explan.doc) }
+/-- Returns an error explanation for the given name if one exists. -/
+def getErrorExplanation? [Monad m] [MonadEnv m] (name : Name) : m (Option ErrorExplanation) := do
+  return errorExplanationExt.getState (← getEnv) |>.find? name
 
-/--
-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.
--/
+@[deprecated getErrorExplanation? (since := "2026-12-20")]
 def getErrorExplanationRaw? (env : Environment) (name : Name) : Option ErrorExplanation := do
   errorExplanationExt.getState env |>.find? name
 
 /-- Returns `true` if there exists an error explanation named `name`. -/
-def hasErrorExplanation [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] (name : Name) : m Bool :=
+def hasErrorExplanation [Monad m] [MonadEnv m] (name : Name) : m Bool :=
   return errorExplanationExt.getState (← getEnv) |>.contains name
 
-/--
-Returns all error explanations with their names as an unsorted array, *without* rewriting manual
-links.
+/-- Returns all error explanations with their names, sorted by name. -/
+public def getErrorExplanations [Monad m] [MonadEnv m] : m (Array (Name × ErrorExplanation)) := do
+  return errorExplanationExt.getState (← getEnv)
+    |>.toArray
+    |>.qsort fun e e' => e.1.toString < e'.1.toString
 
-In general, use `Lean.getErrorExplanations` or `Lean.getErrorExplanationsSorted` instead of this
-function if the bodies of the fetched explanations will be used.
--/
-def getErrorExplanationsRaw (env : Environment) : Array (Name × ErrorExplanation) :=
-  errorExplanationExt.getState env |>.toArray
+@[deprecated getErrorExplanations (since := "2026-12-20")]
+public def getErrorExplanationsRaw (env : Environment) : Array (Name × ErrorExplanation) :=
+  errorExplanationExt.getState env
+    |>.toArray
+    |>.qsort fun e e' => e.1.toString < e'.1.toString
 
-/-- Returns all error explanations with their names, rewriting manual links. -/
-def getErrorExplanations [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] : m (Array (Name × ErrorExplanation)) := do
-  let entries := errorExplanationExt.getState (← getEnv) |>.toArray
-  entries
-    |>.mapM fun (n, e) => return (n, { e with doc := (← rewriteManualLinks e.doc) })
-
-/--
-Returns all error explanations with their names as a sorted array, rewriting manual links.
--/
-def getErrorExplanationsSorted [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] : m (Array (Name × ErrorExplanation)) := do
-  return (← getErrorExplanations).qsort fun e e' => e.1.toString < e'.1.toString
+@[deprecated getErrorExplanations (since := "2026-12-20")]
+public def getErrorExplanationsSorted [Monad m] [MonadEnv m] : m (Array (Name × ErrorExplanation)) := do
+  getErrorExplanations
 
 end Lean
+
+/-
+Error explanations registered in the compiler must be added to the manual and
+referenced in the Manual.ErrorExplanations module here:
+
+https://github.com/leanprover/reference-manual/blob/main/Manual/ErrorExplanations.lean
+
+Details:
+https://github.com/leanprover/reference-manual/blob/main/Manual/ErrorExplanations/README.md
+-/
+
+/-- -/
+register_error_explanation lean.ctorResultingTypeMismatch {
+  summary := "Resulting type of constructor was not the inductive type being declared."
+  sinceVersion := "4.22.0"
+}
+
+/-- -/
+register_error_explanation lean.dependsOnNoncomputable {
+  summary := "Declaration depends on noncomputable definitions but is not marked as noncomputable"
+  sinceVersion := "4.22.0"
+}
+
+/-- -/
+register_error_explanation lean.inductionWithNoAlts {
+  summary := "Induction pattern with nontactic in natural-number-game-style `with` clause."
+  sinceVersion := "4.26.0"
+}
+
+/-- -/
+register_error_explanation lean.inductiveParamMismatch {
+  summary := " Invalid parameter in an occurrence of an inductive type in one of its constructors."
+  sinceVersion := "4.22.0"
+}
+
+/-- -/
+register_error_explanation lean.inductiveParamMissing {
+  summary := "Parameter not present in an occurrence of an inductive type in one of its constructors."
+  sinceVersion := "4.22.0"
+}
+
+/-- -/
+register_error_explanation lean.inferBinderTypeFailed {
+  summary := "The type of a binder could not be inferred."
+  sinceVersion := "4.23.0"
+}
+
+/-- -/
+register_error_explanation lean.inferDefTypeFailed {
+  summary := "The type of a definition could not be inferred."
+  sinceVersion := "4.23.0"
+}
+
+/-- -/
+register_error_explanation lean.invalidDottedIdent {
+  summary := "Dotted identifier notation used with invalid or non-inferrable expected type."
+  sinceVersion := "4.22.0"
+}
+
+/-- -/
+register_error_explanation lean.invalidField {
+  summary := "Generalized field notation used in a potentially ambiguous way."
+  sinceVersion := "4.22.0"
+}
+
+/-- -/
+register_error_explanation lean.projNonPropFromProp {
+  summary := "Tried to project data from a proof."
+  sinceVersion := "4.23.0"
+}
+
+/-- -/
+register_error_explanation lean.propRecLargeElim {
+  summary := "Attempted to eliminate a proof into a higher type universe."
+  sinceVersion := "4.23.0"
+}
+
+/-- -/
+register_error_explanation lean.redundantMatchAlt {
+  summary := "Match alternative will never be reached."
+  sinceVersion := "4.22.0"
+}
+
+/-- -/
+register_error_explanation lean.synthInstanceFailed {
+  summary := "Failed to synthesize instance of type class."
+  sinceVersion := "4.26.0"
+}
+
+/-- -/
+register_error_explanation lean.unknownIdentifier {
+  summary := "Failed to resolve identifier to variable or constant."
+  sinceVersion := "4.23.0"
+}

src/Lean/ErrorExplanations.lean

@@ -1,22 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Joseph Rotella
--/
-module
-
-prelude
-public import Lean.ErrorExplanations.CtorResultingTypeMismatch
-public import Lean.ErrorExplanations.DependsOnNoncomputable
-public import Lean.ErrorExplanations.InductionWithNoAlts
-public import Lean.ErrorExplanations.InductiveParamMismatch
-public import Lean.ErrorExplanations.InductiveParamMissing
-public import Lean.ErrorExplanations.InferBinderTypeFailed
-public import Lean.ErrorExplanations.InferDefTypeFailed
-public import Lean.ErrorExplanations.InvalidDottedIdent
-public import Lean.ErrorExplanations.InvalidField
-public import Lean.ErrorExplanations.ProjNonPropFromProp
-public import Lean.ErrorExplanations.PropRecLargeElim
-public import Lean.ErrorExplanations.RedundantMatchAlt
-public import Lean.ErrorExplanations.SynthInstanceFailed
-public import Lean.ErrorExplanations.UnknownIdentifier

src/Lean/ErrorExplanations/CtorResultingTypeMismatch.lean

@@ -1,72 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Joseph Rotella
--/
-module
-
-prelude
-public import Lean.ErrorExplanation
-meta import Lean.ErrorExplanation
-
-public section
-
-/--
-In an inductive declaration, the resulting type of each constructor must match the type being
-declared; if it does not, this error is raised. That is, every constructor of an inductive type must
-return a value of that type. See the [Inductive Types](lean-manual://section/inductive-types) manual
-section for additional details. Note that it is possible to omit the resulting type for a
-constructor if the inductive type being defined has no indices.
-
-# Examples
-
-## Typo in Resulting Type
-```lean broken
-inductive Tree (α : Type) where
-  | leaf : Tree α
-  | node : α → Tree α → Treee α
-```
-```output
-Unexpected resulting type for constructor `Tree.node`: Expected an application of
-  Tree
-but found
-  ?m.2
-```
-```lean fixed
-inductive Tree (α : Type) where
-  | leaf : Tree α
-  | node : α → Tree α → Tree α
-```
-
-## Missing Resulting Type After Constructor Parameter
-
-```lean broken
-inductive Credential where
-  | pin      : Nat
-  | password : String
-```
-```output
-Unexpected resulting type for constructor `Credential.pin`: Expected
-  Credential
-but found
-  Nat
-```
-```lean fixed (title := "Fixed (resulting type)")
-inductive Credential where
-  | pin      : Nat → Credential
-  | password : String → Credential
-```
-```lean fixed (title := "Fixed (named parameter)")
-inductive Credential where
-  | pin (num : Nat)
-  | password (str : String)
-```
-
-If the type of a constructor is annotated, the full type—including the resulting type—must be
-provided. Alternatively, constructor parameters can be written using named binders; this allows the
-omission of the constructor's resulting type because it contains no indices.
--/
-register_error_explanation lean.ctorResultingTypeMismatch {
-  summary := "Resulting type of constructor was not the inductive type being declared."
-  sinceVersion := "4.22.0"
-}

src/Lean/ErrorExplanations/DependsOnNoncomputable.lean

@@ -1,122 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Joseph Rotella
--/
-module
-
-prelude
-public import Lean.ErrorExplanation
-meta import Lean.ErrorExplanation
-
-public section
-
-/--
-This error indicates that the specified definition depends on one or more definitions that do not
-contain executable code and is therefore required to be marked as `noncomputable`. Such definitions
-can be type-checked but do not contain code that can be executed by Lean.
-
-If you intended for the definition named in the error message to be noncomputable, marking it as
-`noncomputable` will resolve this error. If you did not, inspect the noncomputable definitions on
-which it depends: they may be noncomputable because they failed to compile, are `axiom`s, or were
-themselves marked as `noncomputable`. Making all of your definition's noncomputable dependencies
-computable will also resolve this error. See the manual section on
-[Modifiers](lean-manual://section/declaration-modifiers) for more information about noncomputable
-definitions.
-
-# Examples
-
-## Necessarily Noncomputable Function Not Appropriately Marked
-
-```lean broken
-axiom transform : Nat → Nat
-
-def transformIfZero : Nat → Nat
-  | 0 => transform 0
-  | n => n
-```
-```output
-`transform` not supported by code generator; consider marking definition as `noncomputable`
-```
-```lean fixed
-axiom transform : Nat → Nat
-
-noncomputable def transformIfZero : Nat → Nat
-  | 0 => transform 0
-  | n => n
-```
-In this example, `transformIfZero` depends on the axiom `transform`. Because `transform` is an
-axiom, it does not contain any executable code; although the value `transform 0` has type `Nat`,
-there is no way to compute its value. Thus, `transformIfZero` must be marked `noncomputable` because
-its execution would depend on this axiom.
-
-## Noncomputable Dependency Can Be Made Computable
-
-```lean broken
-noncomputable def getOrDefault [Nonempty α] : Option α → α
-  | some x => x
-  | none => Classical.ofNonempty
-
-def endsOrDefault (ns : List Nat) : Nat × Nat :=
-  let head := getOrDefault ns.head?
-  let tail := getOrDefault ns.getLast?
-  (head, tail)
-```
-```output
-failed to compile definition, consider marking it as 'noncomputable' because it depends on 'getOrDefault', which is 'noncomputable'
-```
-```lean fixed (title := "Fixed (computable)")
-def getOrDefault [Inhabited α] : Option α → α
-  | some x => x
-  | none => default
-
-def endsOrDefault (ns : List Nat) : Nat × Nat :=
-  let head := getOrDefault ns.head?
-  let tail := getOrDefault ns.getLast?
-  (head, tail)
-```
-The original definition of `getOrDefault` is noncomputable due to its use of `Classical.choice`.
-Unlike in the preceding example, however, it is possible to implement a similar but computable
-version of `getOrDefault` (using the `Inhabited` type class), allowing `endsOrDefault` to be
-computable. (The differences between `Inhabited` and `Nonempty` are described in the documentation
-of inhabited types in the manual section on [Basic Classes](lean-manual://section/basic-classes).)
-
-## Noncomputable Instance in Namespace
-
-```lean broken
-open Classical in
-/--
-Returns `y` if it is in the image of `f`,
-or an element of the image of `f` otherwise.
--/
-def fromImage (f : Nat → Nat) (y : Nat) :=
-  if ∃ x, f x = y then
-    y
-  else
-    f 0
-```
-```output
-failed to compile definition, consider marking it as 'noncomputable' because it depends on 'propDecidable', which is 'noncomputable'
-```
-```lean fixed
-open Classical in
-/--
-Returns `y` if it is in the image of `f`,
-or an element of the image of `f` otherwise.
--/
-noncomputable def fromImage (f : Nat → Nat) (y : Nat) :=
-  if ∃ x, f x = y then
-    y
-  else
-    f 0
-```
-The `Classical` namespace contains `Decidable` instances that are not computable. These are a common
-source of noncomputable dependencies that do not explicitly appear in the source code of a
-definition. In the above example, for instance, a `Decidable` instance for the proposition
-`∃ x, f x = y` is synthesized using a `Classical` decidability instance; therefore, `fromImage` must
-be marked `noncomputable`.
--/
-register_error_explanation lean.dependsOnNoncomputable {
-  summary := "Declaration depends on noncomputable definitions but is not marked as noncomputable"
-  sinceVersion := "4.22.0"
-}

src/Lean/ErrorExplanations/InductionWithNoAlts.lean

@@ -1,51 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Rob Simmons
--/
-module
-
-prelude
-public import Lean.ErrorExplanation
-meta import Lean.ErrorExplanation
-
-/--
-Tactic-based proofs using induction in Lean need to use a pattern-matching-like notation to describe
-individual cases of the proof. However, the `induction'` tactic in Mathlib and the specialized
-`induction` tactic for natural numbers used in the Natural Number Game follows a different pattern.
-
-# Examples
-
-## Adding Explicit Cases to an Induction Proof
-
-```lean broken
-theorem zero_mul (m : Nat) : 0 * m = 0 := by
-  induction m with n n_ih
-  rw [Nat.mul_zero]
-  rw [Nat.mul_succ]
-  rw [Nat.add_zero]
-  rw [n_ih]
-```
-```output
-unknown tactic
-```
-```lean fixed
-theorem zero_mul (m : Nat) : 0 * m = 0 := by
-  induction m with
-  | zero =>
-    rw [Nat.mul_zero]
-  | succ n n_ih =>
-    rw [Nat.mul_succ]
-    rw [Nat.add_zero]
-    rw [n_ih]
-```
-The broken example has the structure of a correct proof in the Natural Numbers Game, and this
-proof will work if you `import Mathlib` and replace `induction` with `induction'`. Induction tactics
-in basic Lean expect the `with` keyword to be followed by a series of cases, and the names for
-the inductive case are provided in the `succ` case rather than being provided up-front.
-
--/
-register_error_explanation lean.inductionWithNoAlts {
-  summary := "Induction pattern with nontactic in natural-number-game-style `with` clause."
-  sinceVersion := "4.26.0"
-}

src/Lean/ErrorExplanations/InductiveParamMismatch.lean

@@ -1,62 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Joseph Rotella
--/
-module
-
-prelude
-public import Lean.ErrorExplanation
-meta import Lean.ErrorExplanation
-
-public section
-
-/--
-This error occurs when a parameter of an inductive type is not uniform in an inductive
-declaration. The parameters of an inductive type (i.e., those that appear before the colon following
-the `inductive` keyword) must be identical in all occurrences of the type being defined in its
-constructors' types. If a parameter of an inductive type must vary between constructors, make the
-parameter an index by moving it to the right of the colon. See the manual section on
-[Inductive Types](lean-manual://section/inductive-types) for additional details.
-
-Note that auto-implicit inlay hints always appear left of the colon in an inductive declaration
-(i.e., as parameters), even when they are actually indices. This means that double-clicking on an
-inlay hint to insert such parameters may result in this error. If it does, change the inserted
-parameters to indices.
-
-# Examples
-
-## Vector Length Index as a Parameter
-
-```lean broken
-inductive Vec (α : Type) (n : Nat) : Type where
-  | nil  : Vec α 0
-  | cons : α → Vec α n → Vec α (n + 1)
-```
-```output broken
-Mismatched inductive type parameter in
-  Vec α 0
-The provided argument
-  0
-is not definitionally equal to the expected parameter
-  n
-
-Note: The value of parameter `n` must be fixed throughout the inductive declaration. Consider making this parameter an index if it must vary.
-```
-```lean fixed
-inductive Vec (α : Type) : Nat → Type where
-  | nil  : Vec α 0
-  | cons : α → Vec α n → Vec α (n + 1)
-```
-
-The length argument `n` of the `Vec` type constructor is declared as a parameter, but other values
-for this argument appear in the `nil` and `cons` constructors (namely, `0` and `n + 1`). An error
-therefore appears at the first occurrence of such an argument. To correct this, `n` cannot be a
-parameter of the inductive declaration and must instead be an index, as in the corrected example. On
-the other hand, `α` remains unchanged throughout all occurrences of `Vec` in the declaration and so
-is a valid parameter.
--/
-register_error_explanation lean.inductiveParamMismatch {
-  summary := "Invalid parameter in an occurrence of an inductive type in one of its constructors."
-  sinceVersion := "4.22.0"
-}

src/Lean/ErrorExplanations/InductiveParamMissing.lean

@@ -1,71 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Joseph Rotella
--/
-module
-
-prelude
-public import Lean.ErrorExplanation
-meta import Lean.ErrorExplanation
-
-public section
-
-/--
-This error occurs when an inductive type constructor is partially applied in the type of one of its
-constructors such that one or more parameters of the type are omitted. The elaborator requires that
-all parameters of an inductive type be specified everywhere that type is referenced in its
-definition, including in the types of its constructors.
-
-If it is necessary to allow the type constructor to be partially applied, without specifying a given
-type parameter, that parameter must be converted to an index. See the manual section on
-[Inductive Types](lean-manual://section/inductive-types) for further explanation of the difference
-between indices and parameters.
-
-# Examples
-
-## Omitting Parameter in Argument to Higher-Order Predicate
-
-```lean broken
-inductive List.All {α : Type u} (P : α → Prop) : List α → Prop
-  | nil : All P []
-  | cons {x xs} : P x → All P xs → All P (x :: xs)
-
-structure RoseTree (α : Type u) where
-  val : α
-  children : List (RoseTree α)
-
-inductive RoseTree.All {α : Type u} (P : α → Prop) (t : RoseTree α) : Prop
-  | intro : P t.val → List.All (All P) t.children → All P t
-```
-```output
-Missing parameter(s) in occurrence of inductive type: In the expression
-  List.All (All P) t.children
-found
-  All P
-but expected all parameters to be specified:
-  All P t
-
-Note: All occurrences of an inductive type in the types of its constructors must specify its fixed parameters. Only indices can be omitted in a partial application of the type constructor.
-```
-```lean fixed
-inductive List.All {α : Type u} (P : α → Prop) : List α → Prop
-  | nil : All P []
-  | cons {x xs} : P x → All P xs → All P (x :: xs)
-
-structure RoseTree (α : Type u) where
-  val : α
-  children : List (RoseTree α)
-
-inductive RoseTree.All {α : Type u} (P : α → Prop) : RoseTree α → Prop
-  | intro : P t.val → List.All (All P) t.children → All P t
-```
-Because the `RoseTree.All` type constructor must be partially applied in the argument to `List.All`,
-the unspecified argument (`t`) must not be a parameter of the `RoseTree.All` predicate. Making it an
-index to the right of the colon in the header of `RoseTree.All` allows this partial application to
-succeed.
--/
-register_error_explanation lean.inductiveParamMissing {
-  summary := "Parameter not present in an occurrence of an inductive type in one of its constructors."
-  sinceVersion := "4.22.0"
-}

src/Lean/ErrorExplanations/InferBinderTypeFailed.lean

@@ -1,164 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Joseph Rotella
--/
-module
-
-prelude
-public import Lean.ErrorExplanation
-meta import Lean.ErrorExplanation
-
-public section
-
-/--
-This error occurs when the type of a binder in a declaration header or local binding is not fully
-specified and cannot be inferred by Lean. Generally, this can be resolved by providing more
-information to help Lean determine the type of the binder, either by explicitly annotating its type
-or by providing additional type information at sites where it is used. When the binder in question
-occurs in the header of a declaration, this error is often accompanied by
-[`lean.inferDefTypeFailed`](lean-manual://errorExplanation/lean.inferDefTypeFailed).
-
-Note that if a declaration is annotated with an explicit resulting type—even one that contains
-holes—Lean will not use information from the definition body to infer parameter types. It may
-therefore be necessary to explicitly specify the types of parameters whose types would otherwise be
-inferable without the resulting-type annotation; see the "uninferred binder due to resulting type
-annotation" example below for a demonstration. In `theorem` declarations, the body is never used to
-infer the types of binders, so any binders whose types cannot be inferred from the rest of the
-theorem type must include a type annotation.
-
-This error may also arise when identifiers that were intended to be declaration names are
-inadvertently written in binder position instead. In these cases, the erroneous identifiers are
-treated as binders with unspecified type, leading to a type inference failure. This frequently
-occurs when attempting to simultaneously define multiple constants of the same type using syntax
-that does not support this. Such situations include:
-* Attempting to name an example by writing an identifier after the `example` keyword;
-* Attempting to define multiple constants with the same type and (if applicable) value by listing
-  them sequentially after `def`, `opaque`, or another declaration keyword;
-* Attempting to define multiple fields of a structure of the same type by sequentially listing their
-  names on the same line of a structure declaration; and
-* Omitting vertical bars between inductive constructor names.
-
-The first three cases are demonstrated in examples below.
-
-# Examples
-
-## Binder Type Requires New Type Variable
-
-```lean broken
-def identity x :=
-  x
-```
-```output
-Failed to infer type of binder `x`
-```
-```lean fixed
-def identity (x : α) :=
-  x
-```
-
-In the code above, the type of `x` is unconstrained; as this example demonstrates, Lean does not
-automatically generate fresh type variables for such binders. Instead, the type `α` of `x` must be
-specified explicitly. Note that if automatic implicit parameter insertion is enabled (as it is by
-default), a binder for `α` itself need not be provided; Lean will insert an implicit binder for this
-parameter automatically.
-
-## Uninferred Binder Type Due to Resulting Type Annotation
-
-```lean broken
-def plusTwo x : Nat :=
-  x + 2
-```
-```output
-Failed to infer type of binder `x`
-
-Note: Because this declaration's type has been explicitly provided, all parameter types and holes (e.g., `_`) in its header are resolved before its body is processed; information from the declaration body cannot be used to infer what these values should be
-```
-```lean fixed
-def plusTwo (x : Nat) : Nat :=
-  x + 2
-```
-
-Even though `x` is inferred to have type `Nat` in the body of `plusTwo`, this information is not
-available when elaborating the type of the definition because its resulting type (`Nat`) has been
-explicitly specified. Considering only the information in the header, the type of `x` cannot be
-determined, resulting in the shown error. It is therefore necessary to include the type of `x` in
-its binder.
-
-
-## Attempting to Name an Example Declaration
-
-```lean broken
-example trivial_proof : True :=
-  trivial
-```
-```output
-Failed to infer type of binder `trivial_proof`
-
-Note: Because this declaration's type has been explicitly provided, all parameter types and holes (e.g., `_`) in its header are resolved before its body is processed; information from the declaration body cannot be used to infer what these values should be
-```
-```lean fixed
-example : True :=
-  trivial
-```
-This code is invalid because it attempts to give a name to an `example` declaration. Examples cannot
-be named, and an identifier written where a name would appear in other declaration forms is instead
-elaborated as a binder, whose type cannot be inferred. If a declaration must be named, it should be
-defined using a declaration form that supports naming, such as `def` or `theorem`.
-
-## Attempting to Define Multiple Opaque Constants at Once
-
-```lean broken
-opaque m n : Nat
-```
-```output
-Failed to infer type of binder `n`
-
-Note: Multiple constants cannot be declared in a single declaration. The identifier(s) `n` are being interpreted as parameters `(n : _)`.
-```
-```lean fixed
-opaque m : Nat
-opaque n : Nat
-```
-
-This example incorrectly attempts to define multiple constants with a single `opaque` declaration.
-Such a declaration can define only one constant: it is not possible to list multiple identifiers
-after `opaque` or `def` to define them all to have the same type (or value). Such a declaration is
-instead elaborated as defining a single constant (e.g., `m` above) with parameters given by the
-subsequent identifiers (`n`), whose types are unspecified and cannot be inferred. To define multiple
-global constants, it is necessary to declare each separately.
-
-## Attempting to Define Multiple Structure Fields on the Same Line
-
-```lean broken
-structure Person where
-  givenName familyName : String
-  age : Nat
-```
-```output
-Failed to infer type of binder `familyName`
-```
-```lean fixed (title := "Fixed (separate lines)")
-structure Person where
-  givenName : String
-  familyName : String
-  age : Nat
-```
-```lean fixed (title := "Fixed (parenthesized)")
-structure Person where
-  (givenName familyName : String)
-  age : Nat
-```
-
-This example incorrectly attempts to define multiple structure fields (`givenName` and `familyName`)
-of the same type by listing them consecutively on the same line. Lean instead interprets this as
-defining a single field, `givenName`, parametrized by a binder `familyName` with no specified type.
-The intended behavior can be achieved by either listing each field on a separate line, or enclosing
-the line specifying multiple field names in parentheses (see the manual section on
-[Inductive Types](lean-manual://section/inductive-types) for further details about structure
-declarations).
--/
-register_error_explanation lean.inferBinderTypeFailed {
-  summary := "The type of a binder could not be inferred."
-  sinceVersion := "4.23.0"
-}

src/Lean/ErrorExplanations/InferDefTypeFailed.lean

@@ -1,87 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Joseph Rotella
--/
-module
-
-prelude
-public import Lean.ErrorExplanation
-meta import Lean.ErrorExplanation
-
-public section
-
-/--
-This error occurs when the type of a definition is not fully specified and Lean is unable to infer
-its type from the available information. If the definition has parameters, this error refers only to
-the resulting type after the colon (the error
-[`lean.inferBinderTypeFailed`](lean-manual://errorExplanation/lean.inferBinderTypeFailed) indicates
-that a parameter type could not be inferred).
-
-To resolve this error, provide additional type information in the definition. This can be done
-straightforwardly by providing an explicit resulting type after the colon in the definition
-header. Alternatively, if an explicit resulting type is not provided, adding further type
-information to the definition's body—such as by specifying implicit type arguments or giving
-explicit types to `let` binders—may allow Lean to infer the type of the definition. Look for type
-inference or implicit argument synthesis errors that arise alongside this one to identify
-ambiguities that may be contributing to this error.
-
-Note that when an explicit resulting type is provided—even if that type contains holes—Lean will not
-use information from the definition body to help infer the type of the definition or its parameters.
-Thus, adding an explicit resulting type may also necessitate adding type annotations to parameters
-whose types were previously inferrable. Additionally, it is always necessary to provide an explicit
-type in a `theorem` declaration: the `theorem` syntax requires a type annotation, and the elaborator
-will never attempt to use the theorem body to infer the proposition being proved.
-
-# Examples
-
-## Implicit Argument Cannot be Inferred
-
-```lean broken
-def emptyNats :=
-  []
-```
-```output
-Failed to infer type of definition `emptyNats`
-```
-
-```lean fixed (title := "Fixed (type annotation)")
-def emptyNats : List Nat :=
-  []
-```
-```lean fixed (title := "Fixed (implicit argument)")
-def emptyNats :=
-  List.nil (α := Nat)
-```
-
-Here, Lean is unable to infer the value of the parameter `α` of the `List` type constructor, which
-in turn prevents it from inferring the type of the definition. Two fixes are possible: specifying
-the expected type of the definition allows Lean to infer the appropriate implicit argument to the
-`List.nil` constructor; alternatively, making this implicit argument explicit in the function body
-provides sufficient information for Lean to infer the definition's type.
-
-## Definition Type Uninferrable Due to Unknown Parameter Type
-
-```lean broken
-def identity x :=
-  x
-```
-```output
-Failed to infer type of definition `identity`
-```
-```lean fixed
-def identity (x : α) :=
-  x
-```
-
-In this example, the type of `identity` is determined by the type of `x`, which cannot be inferred.
-Both the indicated error and
-[lean.inferBinderTypeFailed](lean-manual://errorExplanation/lean.inferBinderTypeFailed) therefore
-appear (see that explanation for additional discussion of this example). Resolving the latter—by
-explicitly specifying the type of `x`—provides Lean with sufficient information to infer the
-definition type.
--/
-register_error_explanation lean.inferDefTypeFailed {
-  summary := "The type of a definition could not be inferred."
-  sinceVersion := "4.23.0"
-}

src/Lean/ErrorExplanations/InvalidDottedIdent.lean

@@ -1,78 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Joseph Rotella
--/
-module
-
-prelude
-public import Lean.ErrorExplanation
-meta import Lean.ErrorExplanation
-
-public section
-
-/--
-This error indicates that dotted identifier notation was used in an invalid or unsupported context.
-Dotted identifier notation allows an identifier's namespace to be omitted, provided that it can be
-inferred by Lean based on type information. Details about this notation can be found in the manual
-section on [identifiers](lean-manual://section/identifiers-and-resolution).
-
-This notation can only be used in a term whose type Lean is able to infer. If there is insufficient
-type information for Lean to do so, this error will be raised. The inferred type must not be a type
-universe (e.g., `Prop` or `Type`), as dotted-identifier notation is not supported on these types.
-
-# Examples
-
-## Insufficient Type Information
-
-```lean broken
-def reverseDuplicate (xs : List α) :=
-  .reverse (xs ++ xs)
-```
-```output
-Invalid dotted identifier notation: The expected type of `.reverse` could not be determined
-```
-```lean fixed
-def reverseDuplicate (xs : List α) : List α :=
-  .reverse (xs ++ xs)
-```
-Because the return type of `reverseDuplicate` is not specified, the expected type of `.reverse`
-cannot be determined. Lean will not use the type of the argument `xs ++ xs` to infer the omitted
-namespace. Adding the return type `List α` allows Lean to infer the type of `.reverse` and thus the
-appropriate namespace (`List`) in which to resolve this identifier.
-
-Note that this means that changing the return type of `reverseDuplicate` changes how `.reverse`
-resolves: if the return type is  `T`, then Lean will (attempt to) resolve `.reverse` to a function
-`T.reverse` whose return type is `T`—even if `T.reverse` does not take an argument of type
-`List α`.
-
-## Dotted Identifier Where Type Universe Expected
-
-```lean broken
-example (n : Nat) :=
-  match n > 42 with
-  | .true  => n - 1
-  | .false => n + 1
-```
-```output
-Invalid dotted identifier notation: Not supported on type universe
-  Prop
-```
-```lean fixed
-example (n : Nat) :=
-  match decide (n > 42) with
-  | .true  => n - 1
-  | .false => n + 1
-```
-
-The proposition `n > 42` has type `Prop`, which, being a type universe, does not support
-dotted-identifier notation. As this example demonstrates, attempting to use this notation in such a
-context is almost always an error. The intent in this example was for `.true` and `.false` to be
-Booleans, not propositions; however, `match` expressions do not automatically perform this coercion
-for decidable propositions. Explicitly adding `decide` makes the discriminant a `Bool` and allows
-the dotted-identifier resolution to succeed.
--/
-register_error_explanation lean.invalidDottedIdent {
-  summary := "Dotted identifier notation used with invalid or uninferrable expected type."
-  sinceVersion := "4.22.0"
-}

src/Lean/ErrorExplanations/InvalidField.lean

@@ -1,99 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Rob Simmons
--/
-module
-
-prelude
-public import Lean.ErrorExplanation
-meta import Lean.ErrorExplanation
-
-/--
-This error indicates that an expression containing a dot followed by an identifier was encountered,
-and that it wasn't possible to understand the identifier as a field.
-
-Lean's field notation is very powerful, but this can also make it confusing: the expression
-`color.value` can either be a single [identifier](lean-manual://section/identifiers-and-resolution),
-it can be a reference to the [field of a structure](lean-manual://section/structure-fields), and it
-and be a calling a function on the value `color` with
-[generalized field notation](lean-manual://section/generalized-field-notation).
-
-# Examples
-
-## Incorrect Field Name
-
-```lean broken
-#eval (4 + 2).suc
-```
-```output
-Invalid field `suc`: The environment does not contain `Nat.suc`, so it is not possible to project the field `suc` from an expression
-  4 + 2
-of type `Nat`
-```
-```lean fixed
-#eval (4 + 1).succ
-```
-
-The simplest reason for an invalid field error is that the function being sought, like `Nat.suc`,
-does not exist.
-
-## Projecting from the Wrong Expression
-
-```lean broken
-#eval '>'.leftpad 10 ['a', 'b', 'c']
-```
-```output
-Invalid field `leftpad`: The environment does not contain `Char.leftpad`, so it is not possible to project the field `leftpad` from an expression
-  '>'
-of type `Char`
-```
-```lean fixed
-#eval ['a', 'b', 'c'].leftpad 10 '>'
-```
-
-The type of the expression before the dot entirely determines the function being called by the field
-projection. There is no `Char.leftpad`, and the only way to invoke `List.leftpad` with generalized
-field notation is to have the list come before the dot.
-
-## Type is Not Specific
-
-```lean broken
-def double_plus_one {α} [Add α] (x : α) :=
-   (x + x).succ
-```
-```output
-Invalid field notation: Field projection operates on types of the form `C ...` where C is a constant. The expression
-  x + x
-has type `α` which does not have the necessary form.
-```
-```lean fixed
-def double_plus_one (x : Nat) :=
-   (x + x).succ
-```
-
-The `Add` typeclass is sufficient for performing the addition `x + x`, but the `.succ` field notation
-cannot operate without knowing more about the actual type from which `succ` is being projected.
-
-## Insufficient Type Information
-
-```lean broken
-example := fun (n) => n.succ.succ
-```
-```output
-Invalid field notation: Type of
-  n
-is not known; cannot resolve field `succ`
-```
-```lean fixed
-example := fun (n : Nat) => n.succ.succ
-```
-
-Generalized field notation can only be used when it is possible to determine the type that is being
-projected. Type annotations may need to be added to make generalized field notation work.
-
--/
-register_error_explanation lean.invalidField {
-  summary := "Dotted identifier notation used without ."
-  sinceVersion := "4.22.0"
-}

src/Lean/ErrorExplanations/ProjNonPropFromProp.lean

@@ -1,62 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Joseph Rotella
--/
-module
-
-prelude
-public import Lean.ErrorExplanation
-meta import Lean.ErrorExplanation
-
-public section
-
-/--
-This error occurs when attempting to project a piece of data from a proof of a proposition using an
-index projection. For example, if `h` is a proof of an existential proposition, attempting to
-extract the witness `h.1` is an example of this error. Such projections are disallowed because they
-may violate Lean's prohibition of large elimination from `Prop` (refer to the
-[Propositions](lean-manual://section/propositions) manual section for further details).
-
-Instead of an index projection, consider using a pattern-matching `let`, `match` expression, or a
-destructuring tactic like `cases` to eliminate from one propositional type to another. Note that
-such elimination is only valid if the resulting value is also in `Prop`; if it is not, the error
-[`lean.propRecLargeElim`](lean-manual://errorExplanation/lean.propRecLargeElim) will be raised.
-
-# Examples
-
-## Attempting to Use Index Projection on Existential Proof
-
-```lean broken
-example (a : Nat) (h : ∃ x : Nat, x > a + 1) : ∃ x : Nat, x > 0 :=
-  ⟨h.1, Nat.lt_of_succ_lt h.2⟩
-```
-```output
-Invalid projection: Cannot project a value of non-propositional type
-  Nat
-from the expression
-  h
-which has propositional type
-  ∃ x, x > a + 1
-```
-```lean fixed (title := "Fixed (let)")
-example (a : Nat) (h : ∃ x : Nat, x > a + 1) : ∃ x : Nat, x > a :=
-  let ⟨w, hw⟩ := h
-  ⟨w, Nat.lt_of_succ_lt hw⟩
-```
-```lean (title := "Fixed (cases)")
-example (a : Nat) (h : ∃ x : Nat, x > a + 1) : ∃ x : Nat, x > a := by
-  cases h with
-  | intro w hw =>
-    exists w
-    omega
-```
-
-The witness associated with a proof of an existential proposition cannot be extracted using an
-index projection. Instead, it is necessary to use a pattern match: either a term like a `let`
-binding or a tactic like `cases`.
--/
-register_error_explanation lean.projNonPropFromProp {
-  summary := "Tried to project data from a proof."
-  sinceVersion := "4.23.0"
-}

src/Lean/ErrorExplanations/PropRecLargeElim.lean

@@ -1,131 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Joseph Rotella
--/
-module
-
-prelude
-public import Lean.ErrorExplanation
-meta import Lean.ErrorExplanation
-
-public section
-
-/--
-This error occurs when attempting to eliminate a proof of a proposition into a higher type universe.
-Because Lean's type theory does not allow large elimination from `Prop`, it is invalid to
-pattern-match on such values—e.g., by using `let` or `match`—to produce a piece of data in a
-non-propositional universe (i.e., `Type u`). More precisely, the motive of a propositional recursor
-must be a proposition. (See the manual section on
-[Subsingleton Elimination](lean-manual://section/subsingleton-elimination) for exceptions to this
-rule.)
-
-Note that this error will arise in any expression that eliminates from a proof into a
-non-propositional universe, even if that expression occurs within another expression of
-propositional type (e.g., in a `let` binding in a proof). The "Defining an intermediate data value
-within a proof" example below demonstrates such an occurrence. Errors of this kind can usually be
-resolved by moving the recursor application "outward," so that its motive is the proposition being
-proved rather than the type of data-valued term.
-
-# Examples
-
-## Defining an Intermediate Data Value Within a Proof
-
-```lean broken
-example {α : Type} [inst : Nonempty α] (p : α → Prop) :
-    ∃ x, p x ∨ ¬ p x :=
-  let val :=
-    match inst with
-    | .intro x => x
-  ⟨val, Classical.em (p val)⟩
-```
-```output
-Tactic `cases` failed with a nested error:
-Tactic `induction` failed: recursor `Nonempty.casesOn` can only eliminate into `Prop`
-
-α : Type
-motive : Nonempty α → Sort ?u.48
-h_1 : (x : α) → motive ⋯
-inst✝ : Nonempty α
-⊢ motive inst✝
- after processing
-  _
-the dependent pattern matcher can solve the following kinds of equations
-- <var> = <term> and <term> = <var>
-- <term> = <term> where the terms are definitionally equal
-- <constructor> = <constructor>, examples: List.cons x xs = List.cons y ys, and List.cons x xs = List.nil
-```
-```lean fixed
-example {α : Type} [inst : Nonempty α] (p : α → Prop) :
-    ∃ x, p x ∨ ¬ p x :=
-  match inst with
-  | .intro x => ⟨x, Classical.em (p x)⟩
-```
-Even though the `example` being defined has a propositional type, the body of `val` does not; it has
-type `α : Type`. Thus, pattern-matching on the proof of `Nonempty α` (a proposition) to produce
-`val` requires eliminating that proof into a non-propositional type and is disallowed. Instead, the
-`match` expression must be moved to the top level of the `example`, where the result is a
-`Prop`-valued proof of the existential claim stated in the example's header. This restructuring
-could also be done using a pattern-matching `let` binding.
-
-## Extracting the Witness from an Existential Proof
-
-```lean broken
-def getWitness {α : Type u} {p : α → Prop} (h : ∃ x, p x) : α :=
-  match h with
-  | .intro x _ => x
-```
-```output
-Tactic `cases` failed with a nested error:
-Tactic `induction` failed: recursor `Exists.casesOn` can only eliminate into `Prop`
-
-α : Type u
-p : α → Prop
-motive : (∃ x, p x) → Sort ?u.52
-h_1 : (x : α) → (h : p x) → motive ⋯
-h✝ : ∃ x, p x
-⊢ motive h✝
- after processing
-  _
-the dependent pattern matcher can solve the following kinds of equations
-- <var> = <term> and <term> = <var>
-- <term> = <term> where the terms are definitionally equal
-- <constructor> = <constructor>, examples: List.cons x xs = List.cons y ys, and List.cons x xs = List.nil
-```
-```lean fixed (title := "Fixed (in Prop)")
--- This is `Exists.elim`
-theorem useWitness {α : Type u} {p : α → Prop} {q : Prop}
-    (h : ∃ x, p x) (hq : (x : α) → p x → q) : q :=
-  match h with
-  | .intro x hx => hq x hx
-```
-```lean fixed (title := "Fixed (in Type)")
-def getWitness {α : Type u} {p : α → Prop}
-    (h : (x : α) ×' p x) : α :=
-  match h with
-  | .mk x _ => x
-```
-In this example, simply relocating the pattern-match is insufficient; the attempted definition
-`getWitness` is fundamentally unsound. (Consider the case where `p` is `fun (n : Nat) => n > 0`: if
-`h` and `h'` are proofs of `∃ x, x > 0`, with `h` using witness `1` and `h'` witness `2`, then since
-`h = h'` by proof irrelevance, it follows that `getWitness h = getWitness h'`—i.e., `1 = 2`.)
-
-Instead, `getWitness` must be rewritten: either the resulting type of the function must be a
-proposition (the first fixed example above), or `h` must not be a proposition (the second).
-
-In the first corrected example, the resulting type of `useWitness` is now a proposition `q`. This
-allows us to pattern-match on `h`—since we are eliminating into a propositional type—and pass the
-unpacked values to `hq`. From a programmatic perspective, one can view `useWitness` as rewriting
-`getWitness` in continuation-passing style, restricting subsequent computations to use its result
-only to construct values in `Prop`, as required by the prohibition on propositional large
-elimination. Note that `useWitness` is the existential elimination principle `Exists.elim`.
-
-The second corrected example changes the type of `h` from an existential proposition to a
-`Type`-valued dependent pair (corresponding to the `PSigma` type constructor). Since this type is
-not propositional, eliminating into `α : Type u` is no longer invalid, and the previously attempted
-pattern match now type-checks.
--/
-register_error_explanation lean.propRecLargeElim {
-  summary := "Attempted to eliminate a proof into a higher type universe."
-  sinceVersion := "4.23.0"
-}

src/Lean/ErrorExplanations/README.md

@@ -1,95 +0,0 @@
-# Error Explanations
-
-## Overview
-
-This directory contains explanations for named errors in Lean core.
-Explanations associate to each named error or warning a long-form
-description of its meaning and causes, relevant background
-information, and strategies for correcting erroneous code. They also
-provide examples of incorrect and corrected code. While error
-explanations are declared in source, they are viewed as part of
-external documentation linked from error messages.
-
-Explanations straddle the line between diagnostics and documentation:
-unlike the error messages they describe, explanations serve not only
-to aid the debugging process but also to help users understand the
-principles of the language that underlie the error. Accordingly, error
-explanations should be written with both of these aims in mind. Refer
-to existing explanations for examples of the formatting and content
-conventions described here.
-
-Once an error explanation has been registered, use the macros
-`throwNamedError`, `logNamedError`, `throwNamedErrorAt` and
-`logNamedErrorAt` to tag error messages with the appropriate
-explanation name. Doing so will display a widget in the Infoview with
-the name of the error and a link to the corresponding explanation.
-
-## Registering Explanations
-
-New error explanations are declared using the
-`register_error_explanation` command. Each explanation should
-appear in a separate submodule of `Lean.ErrorExplanations` whose name
-matches the error name being declared; the module should be marked
-with `prelude` and import only `Lean.ErrorExplanation`. The
-`register_error_explanation` keyword is preceded by a doc
-comment containing the explanation (written in Markdown, following the
-structure guidelines below) and is followed by the name of the
-explanation and a `Lean.ErrorExplanation.Metadata` structure
-describing the error. All errors have two-component names: the first
-identifies the package or "domain" to which the error belongs (in
-core, this will nearly always be `lean`); the second identifies the
-error itself. Error names are written in upper camel case and should
-be descriptive but not excessively verbose. Abbreviations in error
-names are acceptable, but they should be reasonably clear (e.g.,
-abbreviations that are commonly used elsewhere in Lean, such as `Ctor`
-for "constructor") and should not be ambiguous with other vocabulary
-likely to appear in error names (e.g., use `Indep` rather than `Ind`
-for "independent," since the latter could be confused with
-"inductive").
-
-
-## Structure
-
-### Descriptions
-
-Error explanations consist of two parts: a prose description of the
-error and code examples. The description should begin by explaining
-the meaning of the error and why it occurs. It should also briefly
-explain, if appropriate, any relevant context, such as related errors
-or relevant entries in the reference manual. The latter is especially
-useful for directing users to important concepts for understanding an
-error: while it is appropriate to provide brief conceptual exposition
-in an error explanation, avoid extensively duplicating content that
-can be found elsewhere in the manual. General resolution or debugging
-strategies not tied to specific examples can also be discussed in the
-description portion of an explanation.
-
-### Examples
-
-The second half of an explanation (set off by the level-1 header
-"Examples") contains annotated code examples. Each of these consists
-of a level-2 header with the name of the example, followed immediately
-by a sequence of code blocks containing self-contained minimal working
-(or error-producing) examples (MWEs) and outputs. The first MWE should
-have the Markdown info string `lean broken` and demonstrate the error
-in question; it should be followed by an `output` code block with the
-corresponding error message. Subsequent MWEs should have the info
-string `lean fixed` and illustrate how to rewrite the code correctly.
-Finally, after these MWEs, include explanatory text describing the
-example and the cause and resolution of the error it demonstrates.
-
-Note that each MWE in an example will be rendered as a tab, and the
-full example (including its explanatory text) will appear in a
-collapsible "Example" block like those used elsewhere in the manual.
-Include `(title := "Title")` in the info string of an MWE to assign it
-a custom title (for instance, if there are multiple "fixed" MWEs).
-Examples should center on code: prose not specific to the example
-should generally appear in the initial half of the explanation.
-However, an example should provide sufficient commentary for users to
-understand how it illustrates relevant ideas from the preceding
-description and what was done to resolve the exemplified error.
-
-Choose examples carefully: they should be relatively minimal, so as to
-draw out the error itself, but not so contrived as to impede
-comprehension. Each should contain a distinct, representative instance
-of the error to avoid the need for excessively many.

src/Lean/ErrorExplanations/RedundantMatchAlt.lean

@@ -1,120 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Joseph Rotella
--/
-module
-
-prelude
-public import Lean.ErrorExplanation
-meta import Lean.ErrorExplanation
-
-public section
-
-/--
-This error occurs when an alternative in a pattern match can never be reached: any values that would
-match the provided patterns would also match some preceding alternative. Refer to the
-[Pattern Matching](lean-manual://section/pattern-matching) manual section for additional details
-about pattern matching.
-
-This error may appear in any pattern matching expression, including `match` expressions, equational
-function definitions, `if let` bindings, and monadic `let` bindings with fallback clauses.
-
-In pattern-matches with multiple arms, this error may occur if a less-specific pattern precedes a
-more-specific one that it subsumes. Bear in mind that expressions are matched against patterns from
-top to bottom, so specific patterns should precede generic ones.
-
-In `if let` bindings and monadic `let` bindings with fallback clauses, in which only one pattern is
-specified, this error indicates that the specified pattern will always be matched. In this case, the
-binding in question can be replaced with a standard pattern-matching `let`.
-
-One common cause of this error is that a pattern that was intended to match a constructor was
-instead interpreted as a variable binding. This occurs, for instance, if a constructor
-name (e.g., `cons`) is written without its prefix (`List`) outside of that type's namespace. The
-constructor-name-as-variable linter, enabled by default, will display a warning on any variable
-patterns that resemble constructor names.
-
-This error nearly always indicates an issue with the code where it appears. If needed, however,
-`set_option match.ignoreUnusedAlts true` will disable the check for this error and allow pattern
-matches with redundant alternatives to be compiled by discarding the unused arms.
-
-# Examples
-
-## Incorrect Ordering of Pattern Matches
-
-```lean broken
-def seconds : List (List α) → List α
-  | [] => []
-  | _ :: xss => seconds xss
-  | (_ :: x :: _) :: xss => x :: seconds xss
-```
-```output
-Redundant alternative: Any expression matching
-  (head✝ :: x :: tail✝) :: xss
-will match one of the preceding alternatives
-```
-```lean fixed
-def seconds : List (List α) → List α
-  | [] => []
-  | (_ :: x :: _) :: xss => x :: seconds xss
-  | _ :: xss => seconds xss
-```
-
-Since any expression matching `(_ :: x :: _) :: xss` will also match `_ :: xss`, the last
-alternative in the broken implementation is never reached. We resolve this by moving the more
-specific alternative before the more general one.
-
-## Unnecessary Fallback Clause
-
-```lean broken
-example (p : Nat × Nat) : IO Nat := do
-  let (m, n) := p
-    | return 0
-  return m + n
-```
-```output
-Redundant alternative: Any expression matching
-  x✝
-will match one of the preceding alternatives
-```
-```lean fixed
-example (p : Nat × Nat) : IO Nat := do
-  let (m, n) := p
-  return m + n
-```
-
-Here, the fallback clause serves as a catch-all for all values of `p` that do not match `(m, n)`.
-However, no such values exist, so the fallback clause is unnecessary and can be removed. A similar
-error arises when using `if let pat := e` when `e` will always match `pat`.
-
-## Pattern Treated as Variable, Not Constructor
-
-```lean broken
-example (xs : List Nat) : Bool :=
-  match xs with
-  | nil => false
-  | _ => true
-```
-```output
-Redundant alternative: Any expression matching
-  x✝
-will match one of the preceding alternatives
-```
-```lean fixed
-example (xs : List Nat) : Bool :=
-  match xs with
-  | .nil => false
-  | _ => true
-```
-
-In the original example, `nil` is treated as a variable, not as a constructor name, since this
-definition is not within the `List` namespace. Thus, all values of `xs` will match the first
-pattern, rendering the second unused. Notice that the constructor-name-as-variable linter displays a
-warning at `nil`, indicating its similarity to a valid constructor name. Using dot-prefix notation,
-as shown in the fixed example, or specifying the full constructor name `List.nil` achieves the
-intended behavior.
--/
-register_error_explanation lean.redundantMatchAlt {
-  summary := "Match alternative will never be reached."
-  sinceVersion := "4.22.0"
-}

src/Lean/ErrorExplanations/SynthInstanceFailed.lean

@@ -1,125 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Rob Simmons
--/
-module
-
-prelude
-public import Lean.ErrorExplanation
-meta import Lean.ErrorExplanation
-
-public section
-
-/--
-[Type classes](lean-manual://section/type-class) are the mechanism that Lean and many other
-programming languages use to handle overloaded operations. The code that handles a particular
-overloaded operation is an _instance_ of a typeclass; deciding which instance to use for a given
-overloaded operation is called _synthesizing_ an instance.
-
-As an example, when Lean encounters an expression `x + y` where `x` and `y` both have type `Int`,
-it is necessary to look up how it should add two integers and also look up what the resulting type
-will be. This is described as synthesizing an instance of the type class `HAdd Int Int t` for some
-type `t`.
-
-Many failures to synthesize an instance of a type class are the result of using the wrong binary
-operation. Both success and failure are not always straightforward, because some instances are
-defined in terms of other instances, and Lean must recursively search to find appropriate instances.
-It's possible to inspect Lean's instance synthesis](lean-manual://section/instance-search), and this
-can be helpful for diagnosing tricky failures of type class instance synthesis.
-
-# Examples
-
-## Using the Wrong Binary Operation
-
-```lean broken
-#eval "A" + "3"
-```
-```output
-failed to synthesize instance of type class
-  HAdd String String ?m.4
-
-Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
-```
-```lean fixed
-#eval "A" ++ "3"
-```
-
-The binary operation `+` is associated with the `HAdd` type class, and there's no way to add two
-strings. The binary operation `++`, associated with the `HAppend` type class, is the correct way to
-append strings.
-
-## Arguments Have the Wrong Type
-
-```lean broken
-def x : Int := 3
-#eval x ++ "meters"
-```
-```output
-failed to synthesize instance of type class
-  HAppend Int String ?m.4
-
-Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
-```
-```lean fixed
-def x : Int := 3
-#eval ToString.toString x ++ "meters"
-```
-
-Lean does not allow integers and strings to be added directly. The function `ToString.toString` uses
-type class overloading to convert values to strings; by successfully searching for an instance of
-`ToString Int`, the second example will succeed.
-
-## Missing Type Class Instance
-
-```lean broken
-inductive MyColor where
-  | chartreuse | sienna | thistle
-
-def forceColor (oc : Option MyColor) :=
-  oc.get!
-```
-```output
-failed to synthesize instance of type class
-  Inhabited MyColor
-
-Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
-```
-```lean fixed (title := "Fixed (derive instance when defining type)")
-inductive MyColor where
-  | chartreuse | sienna | thistle
-deriving Inhabited
-
-def forceColor (oc : Option MyColor) :=
-  oc.get!
-```
-```lean fixed (title := "Fixed (derive instance separately)")
-inductive MyColor where
-  | chartreuse | sienna | thistle
-
-deriving instance Inhabited for MyColor
-
-def forceColor (oc : Option MyColor) :=
-  oc.get!
-```
-```lean fixed (title := "Fixed (define instance)")
-inductive MyColor where
-  | chartreuse | sienna | thistle
-
-instance : Inhabited MyColor where
-  default := .sienna
-
-def forceColor (oc : Option MyColor) :=
-  oc.get!
-```
-
-Type class synthesis can fail because an instance of the type class simply needs to be provided.
-This commonly happens for type classes like `Repr`, `BEq`, `ToJson` and `Inhabited`. Lean can often
-[automatically generate instances of the type class with the `deriving` keyword](lean-manual://section/type-class),
-either when the type is defined or with the stand-alone `deriving` command.
-
--/
-register_error_explanation lean.synthInstanceFailed {
-  summary := "Failed to synthesize instance of type class"
-  sinceVersion := "4.26.0"
-}

src/Lean/ErrorExplanations/UnknownIdentifier.lean

@@ -1,236 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Joseph Rotella
--/
-module
-
-prelude
-public import Lean.ErrorExplanation
-meta import Lean.ErrorExplanation
-
-/--
-This error means that Lean was unable to find a variable or constant matching the given name. More
-precisely, this means that the name could not be *resolved*, as described in the manual section on
-[Identifiers](lean-manual://section/identifiers-and-resolution): no interpretation of the input as
-the name of a local or section variable (if applicable), a previously declared global constant, or a
-projection of either of the preceding was valid. ("If applicable" refers to the fact that in some
-cases—e.g., the `#print` command's argument—names are resolved only to global constants.)
-
-Note that this error message will display only one possible resolution of the identifier, but the
-presence of this error indicates failures for *all* possible names to which it might refer. For
-example, if the identifier `x` is entered with the namespaces `A` and `B` are open, the error
-message "Unknown identifier \`x\`" indicates that none of `x`, `A.x`, or `B.x` could be found (or
-that `A.x` or `B.x`, if either exists, is a protected declaration).
-
-Common causes of this error include forgetting to import the module in which a constant is defined,
-omitting a constant's namespace when that namespace is not open, or attempting to refer to a local
-variable that is not in scope.
-
-To help resolve some of these common issues, this error message is accompanied by a code action that
-suggests constant names similar to the one provided. These include constants in the environment as
-well as those that can be imported from other modules. Note that these suggestions are available
-only through supported code editors' built-in code action mechanisms and not as a hint in the error
-message itself.
-
-# Examples
-
-## Missing Import
-
-```lean broken
-def inventory :=
-  Std.HashSet.ofList [("apples", 3), ("bananas", 4)]
-```
-```output
-Unknown identifier `Std.HashSet.ofList`
-```
-```lean fixed
-public import Std.Data.HashSet.Basic
-
-public section
-
-def inventory :=
-  Std.HashSet.ofList [("apples", 3), ("bananas", 4)]
-```
-The constant `Std.HashSet.ofList` is defined in the `Std.Data.HashSet.Basic` module, which has not
-been imported in the original example. This import is suggested by the unknown identifier code
-action; once it is added, this example compiles.
-
-## Variable Not in Scope
-
-```lean broken
-example (s : IO.FS.Stream) := do
-  IO.withStdout s do
-    let text := "Hello"
-    IO.println text
-  IO.println s!"Wrote '{text}' to stream"
-```
-```output
-Unknown identifier `text`
-```
-```lean fixed
-example (s : IO.FS.Stream) := do
-  let text := "Hello"
-  IO.withStdout s do
-    IO.println text
-  IO.println s!"Wrote '{text}' to stream"
-```
-An unknown identifier error occurs on the last line of this example because the variable `text` is
-not in scope. The `let`-binding on the third line is scoped to the inner `do` block and cannot be
-accessed in the outer `do` block. Moving this binding to the outer `do` block—from which it remains
-in scope in the inner block as well—resolves the issue.
-
-## Missing Namespace
-
-```lean broken
-inductive Color where
-  | rgb (r g b : Nat)
-  | grayscale (k : Nat)
-
-def red : Color :=
-  rgb 255 0 0
-```
-```output
-Unknown identifier `rgb`
-```
-```lean fixed (title := "Fixed (qualified name)")
-inductive Color where
-  | rgb (r g b : Nat)
-  | grayscale (k : Nat)
-
-def red : Color :=
-  Color.rgb 255 0 0
-```
-```lean fixed (title := "Fixed (open namespace)")
-inductive Color where
-  | rgb (r g b : Nat)
-  | grayscale (k : Nat)
-
-open Color in
-def red : Color :=
-  rgb 255 0 0
-```
-
-In this example, the identifier `rgb` on the last line does not resolve to the `Color` constructor
-of that name. This is because the constructor's name is actually `Color.rgb`: all constructors of an
-inductive type have names in that type's namespace. Because the `Color` namespace is not open, the
-identifier `rgb` cannot be used without its namespace prefix.
-
-One way to resolve this error is to provide the fully qualified constructor name `Color.rgb`; the
-dotted-identifier notation `.rgb` can also be used, since the expected type of `.rgb 255 0 0` is
-`Color`. Alternatively, one can open the `Color` namespace and continue to omit the `Color` prefix
-from the identifier.
-
-## Protected Constant Name Without Namespace Prefix
-
-```lean broken
-protected def A.x := ()
-
-open A
-
-example := x
-```
-```output
-Unknown identifier `x`
-```
-```lean fixed (title := "Fixed (qualified name)")
-protected def A.x := ()
-
-open A
-
-example := A.x
-```
-```lean fixed (title := "Fixed (restricted open)")
-protected def A.x := ()
-
-open A (x)
-
-example := x
-```
-
-In this example, because the constant `A.x` is `protected`, it cannot be referred to by the suffix
-`x` even with the namespace `A` open. Therefore, the identifier `x` fails to resolve. Instead, to
-refer to a `protected` constant, it is necessary to include at least its innermost namespace—in this
-case, `A`. Alternatively, the *restricted opening* syntax—demonstrated in the second corrected
-example—allows a `protected` constant to be referred to by its unqualified name, without opening the
-remainder of the namespace in which it occurs (see the manual section on
-[Namespaces and Sections](lean-manual://section/namespaces-sections) for details).
-
-## Unresolvable Name Inferred by Dotted-Identifier Notation
-
-```lean broken
-def disjoinToNat (b₁ b₂ : Bool) : Nat :=
-  .toNat (b₁ || b₂)
-```
-```output
-Unknown constant `Nat.toNat`
-
-Note: Inferred this name from the expected resulting type of `.toNat`:
-  Nat
-```
-```lean fixed (title := "Fixed (generalized field notation)")
-def disjoinToNat (b₁ b₂ : Bool) : Nat :=
-  (b₁ || b₂).toNat
-```
-```lean fixed (title := "Fixed (qualified name)")
-def disjoinToNat (b₁ b₂ : Bool) : Nat :=
-  Bool.toNat (b₁ || b₂)
-```
-
-In this example, the dotted-identifier notation `.toNat` causes Lean to infer an unresolvable
-name (`Nat.toNat`). The namespace used by dotted-identifier notation is always inferred from
-the expected type of the expression in which it occurs, which—due to the type annotation on
-`disjoinToNat`—is `Nat` in this example. To use the namespace of an argument's type—as the author of
-this code seemingly intended—use *generalized field notation* as shown in the first corrected
-example. Alternatively, the correct namespace can be explicitly specified by writing the fully
-qualified function name.
-
-## Auto-bound variables
-
-```lean broken
-set_option relaxedAutoImplicit false in
-def thisBreaks (x : α₁) (y : size₁) := ()
-
-set_option autoImplicit false in
-def thisAlsoBreaks (x : α₂) (y : size₂) := ()
-```
-```output
-Unknown identifier `size₁`
-
-Note: It is not possible to treat `size₁` as an implicitly bound variable here because it has multiple characters while the `relaxedAutoImplicit` option is set to `false`.
-Unknown identifier `α₂`
-
-Note: It is not possible to treat `α₂` as an implicitly bound variable here because the `autoImplicit` option is set to `false`.
-Unknown identifier `size₂`
-
-Note: It is not possible to treat `size₂` as an implicitly bound variable here because the `autoImplicit` option is set to `false`.
-```
-```lean fixed (title := "Fixed (modifying options)")
-set_option relaxedAutoImplicit true in
-def thisWorks (x : α₁) (y : size₁) := ()
-
-set_option autoImplicit true in
-def thisAlsoWorks (x : α₂) (y : size₂) := ()
-```
-```lean fixed (title := "Fixed (add implicit bindings for the unknown identifiers)")
-set_option relaxedAutoImplicit false in
-def thisWorks {size₁} (x : α₁) (y : size₁) := ()
-
-set_option autoImplicit false in
-def thisAlsoWorks {α₂ size₂} (x : α₂) (y : size₂) := ()
-```
-
-Lean's default behavior, when it encounters an identifier it can't identify in the type of a
-definition, is to add [automatic implicit parameters](lean-manual://section/automatic-implicit-parameters)
-for those unknown identifiers. However, many files or projects disable this feature by setting the
-`autoImplicit` or `relaxedAutoImplicit` options to `false`.
-
-Without re-enabling the `autoImplicit` or `relaxedAutoImplicit` options, the easiest way to fix
-this error is to add the unknown identifiers as [ordinary implicit parameters](lean-manual://section/implicit-functions)
-as shown in the example above.
-
--/
-register_error_explanation lean.unknownIdentifier {
-  summary := "Failed to resolve identifier to variable or constant."
-  sinceVersion := "4.23.0"
-}

src/Lean/Exception.lean

@@ -9,7 +9,7 @@ prelude
 public import Lean.InternalExceptionId
 -- This import is necessary to ensure that any users of the `throwNamedError` macros have access to
 -- all declared explanations:
-public import Lean.ErrorExplanations
+public import Lean.ErrorExplanation
 
 public section
 

src/Lean/Log.lean

@@ -8,7 +8,7 @@ module
 prelude
 -- This import is necessary to ensure that any users of the `logNamedError` macros have access to
 -- all declared explanations:
-public import Lean.ErrorExplanations
+public import Lean.ErrorExplanation
 
 public section
 

src/Lean/Parser/Command.lean

@@ -964,7 +964,7 @@ Registers an error explanation.
 Note that the error name is not relativized to the current namespace.
 -/
 @[builtin_command_parser] def registerErrorExplanationStx := leading_parser
-  docComment >> "register_error_explanation " >> ident >> termParser
+  optional docComment >> "register_error_explanation " >> ident >> termParser
 
 /--
 Returns syntax for `private` or `public` visibility depending on `isPublic`. This function should be

src/Lean/Server/Completion/CompletionCollectors.lean

@@ -571,7 +571,7 @@ def errorNameCompletion
     (caps              : ClientCapabilities)
     : IO (Array ResolvableCompletionItem) :=
   ctx.runMetaM {} do
-    let explanations := getErrorExplanationsRaw (← getEnv)
+    let explanations ← getErrorExplanations
     return trailingDotCompletion explanations partialId caps ctx fun name explan textEdit? => {
       label := name.toString,
       detail? := "error name",

src/Lean/Server/GoTo.lean

@@ -194,7 +194,7 @@ where
 
 def locationLinksFromErrorNameInfo (eni : ErrorNameInfo) : GoToM (Array LeanLocationLink) := do
   let ctx ← read
-  let some explan := getErrorExplanationRaw? (← getEnv) eni.errorName
+  let some explan ← getErrorExplanation? eni.errorName
     | return #[]
   let some loc := explan.declLoc?
     | return #[]

src/Lean/Server/InfoUtils.lean

@@ -342,7 +342,7 @@ def Info.docString? (i : Info) : MetaM (Option String) := do
       return decl.fullDescr
     return none
   | .ofErrorNameInfo eni => do
-    let some errorExplanation := getErrorExplanationRaw? (← getEnv) eni.errorName | return none
+    let some errorExplanation ← getErrorExplanation? eni.errorName | return none
     return errorExplanation.summaryWithSeverity
   | .ofDocInfo di =>
     return (← findDocString? env di.stx.getKind)

tests/lean/interactive/errorExplanationInteractive.lean.expected.out

@@ -2,19 +2,6 @@
  "position": {"line": 28, "character": 30}}
 {"items":
  [{"textEdit":
-   {"replace":
-    {"start": {"line": 28, "character": 23},
-     "end": {"line": 28, "character": 30}},
-    "newText": "testPkg.foo2",
-    "insert":
-    {"start": {"line": 28, "character": 23},
-     "end": {"line": 28, "character": 30}}},
-   "label": "testPkg.foo2",
-   "kind": 10,
-   "documentation": {"value": "(error) Error 2", "kind": "markdown"},
-   "detail": "error name",
-   "data": ["«external:file:///errorExplanationInteractive.lean»", 28, 30, 0]},
-  {"textEdit":
    {"replace":
     {"start": {"line": 28, "character": 23},
      "end": {"line": 28, "character": 30}},
@@ -39,22 +26,21 @@
    "kind": 10,
    "documentation": {"value": "(error) Error 1", "kind": "markdown"},
    "detail": "error name",
+   "data": ["«external:file:///errorExplanationInteractive.lean»", 28, 30, 0]},
+  {"textEdit":
+   {"replace":
+    {"start": {"line": 28, "character": 23},
+     "end": {"line": 28, "character": 30}},
+    "newText": "testPkg.foo2",
+    "insert":
+    {"start": {"line": 28, "character": 23},
+     "end": {"line": 28, "character": 30}}},
+   "label": "testPkg.foo2",
+   "kind": 10,
+   "documentation": {"value": "(error) Error 2", "kind": "markdown"},
+   "detail": "error name",
    "data": ["«external:file:///errorExplanationInteractive.lean»", 28, 30, 0]}],
  "isIncomplete": false}
-Resolution of testPkg.foo2:
-{"textEdit":
- {"replace":
-  {"start": {"line": 28, "character": 23},
-   "end": {"line": 28, "character": 30}},
-  "newText": "testPkg.foo2",
-  "insert":
-  {"start": {"line": 28, "character": 23},
-   "end": {"line": 28, "character": 30}}},
- "label": "testPkg.foo2",
- "kind": 10,
- "documentation": {"value": "(error) Error 2", "kind": "markdown"},
- "detail": "error name",
- "data": ["«external:file:///errorExplanationInteractive.lean»", 28, 30, 0]}
 Resolution of testPkg.bar:
 {"textEdit":
  {"replace":
@@ -83,23 +69,24 @@ Resolution of testPkg.foo1:
  "documentation": {"value": "(error) Error 1", "kind": "markdown"},
  "detail": "error name",
  "data": ["«external:file:///errorExplanationInteractive.lean»", 28, 30, 0]}
+Resolution of testPkg.foo2:
+{"textEdit":
+ {"replace":
+  {"start": {"line": 28, "character": 23},
+   "end": {"line": 28, "character": 30}},
+  "newText": "testPkg.foo2",
+  "insert":
+  {"start": {"line": 28, "character": 23},
+   "end": {"line": 28, "character": 30}}},
+ "label": "testPkg.foo2",
+ "kind": 10,
+ "documentation": {"value": "(error) Error 2", "kind": "markdown"},
+ "detail": "error name",
+ "data": ["«external:file:///errorExplanationInteractive.lean»", 28, 30, 0]}
 {"textDocument": {"uri": "file:///errorExplanationInteractive.lean"},
  "position": {"line": 30, "character": 31}}
 {"items":
  [{"textEdit":
-   {"replace":
-    {"start": {"line": 30, "character": 23},
-     "end": {"line": 30, "character": 31}},
-    "newText": "testPkg.foo2",
-    "insert":
-    {"start": {"line": 30, "character": 23},
-     "end": {"line": 30, "character": 31}}},
-   "label": "testPkg.foo2",
-   "kind": 10,
-   "documentation": {"value": "(error) Error 2", "kind": "markdown"},
-   "detail": "error name",
-   "data": ["«external:file:///errorExplanationInteractive.lean»", 30, 31, 0]},
-  {"textEdit":
    {"replace":
     {"start": {"line": 30, "character": 23},
      "end": {"line": 30, "character": 31}},
@@ -124,22 +111,21 @@ Resolution of testPkg.foo1:
    "kind": 10,
    "documentation": {"value": "(error) Error 1", "kind": "markdown"},
    "detail": "error name",
+   "data": ["«external:file:///errorExplanationInteractive.lean»", 30, 31, 0]},
+  {"textEdit":
+   {"replace":
+    {"start": {"line": 30, "character": 23},
+     "end": {"line": 30, "character": 31}},
+    "newText": "testPkg.foo2",
+    "insert":
+    {"start": {"line": 30, "character": 23},
+     "end": {"line": 30, "character": 31}}},
+   "label": "testPkg.foo2",
+   "kind": 10,
+   "documentation": {"value": "(error) Error 2", "kind": "markdown"},
+   "detail": "error name",
    "data": ["«external:file:///errorExplanationInteractive.lean»", 30, 31, 0]}],
  "isIncomplete": false}
-Resolution of testPkg.foo2:
-{"textEdit":
- {"replace":
-  {"start": {"line": 30, "character": 23},
-   "end": {"line": 30, "character": 31}},
-  "newText": "testPkg.foo2",
-  "insert":
-  {"start": {"line": 30, "character": 23},
-   "end": {"line": 30, "character": 31}}},
- "label": "testPkg.foo2",
- "kind": 10,
- "documentation": {"value": "(error) Error 2", "kind": "markdown"},
- "detail": "error name",
- "data": ["«external:file:///errorExplanationInteractive.lean»", 30, 31, 0]}
 Resolution of testPkg.bar:
 {"textEdit":
  {"replace":
@@ -168,23 +154,24 @@ Resolution of testPkg.foo1:
  "documentation": {"value": "(error) Error 1", "kind": "markdown"},
  "detail": "error name",
  "data": ["«external:file:///errorExplanationInteractive.lean»", 30, 31, 0]}
+Resolution of testPkg.foo2:
+{"textEdit":
+ {"replace":
+  {"start": {"line": 30, "character": 23},
+   "end": {"line": 30, "character": 31}},
+  "newText": "testPkg.foo2",
+  "insert":
+  {"start": {"line": 30, "character": 23},
+   "end": {"line": 30, "character": 31}}},
+ "label": "testPkg.foo2",
+ "kind": 10,
+ "documentation": {"value": "(error) Error 2", "kind": "markdown"},
+ "detail": "error name",
+ "data": ["«external:file:///errorExplanationInteractive.lean»", 30, 31, 0]}
 {"textDocument": {"uri": "file:///errorExplanationInteractive.lean"},
  "position": {"line": 32, "character": 32}}
 {"items":
  [{"textEdit":
-   {"replace":
-    {"start": {"line": 32, "character": 23},
-     "end": {"line": 32, "character": 32}},
-    "newText": "testPkg.foo2",
-    "insert":
-    {"start": {"line": 32, "character": 23},
-     "end": {"line": 32, "character": 32}}},
-   "label": "testPkg.foo2",
-   "kind": 10,
-   "documentation": {"value": "(error) Error 2", "kind": "markdown"},
-   "detail": "error name",
-   "data": ["«external:file:///errorExplanationInteractive.lean»", 32, 32, 0]},
-  {"textEdit":
    {"replace":
     {"start": {"line": 32, "character": 23},
      "end": {"line": 32, "character": 32}},
@@ -196,22 +183,21 @@ Resolution of testPkg.foo1:
    "kind": 10,
    "documentation": {"value": "(error) Error 1", "kind": "markdown"},
    "detail": "error name",
+   "data": ["«external:file:///errorExplanationInteractive.lean»", 32, 32, 0]},
+  {"textEdit":
+   {"replace":
+    {"start": {"line": 32, "character": 23},
+     "end": {"line": 32, "character": 32}},
+    "newText": "testPkg.foo2",
+    "insert":
+    {"start": {"line": 32, "character": 23},
+     "end": {"line": 32, "character": 32}}},
+   "label": "testPkg.foo2",
+   "kind": 10,
+   "documentation": {"value": "(error) Error 2", "kind": "markdown"},
+   "detail": "error name",
    "data": ["«external:file:///errorExplanationInteractive.lean»", 32, 32, 0]}],
  "isIncomplete": false}
-Resolution of testPkg.foo2:
-{"textEdit":
- {"replace":
-  {"start": {"line": 32, "character": 23},
-   "end": {"line": 32, "character": 32}},
-  "newText": "testPkg.foo2",
-  "insert":
-  {"start": {"line": 32, "character": 23},
-   "end": {"line": 32, "character": 32}}},
- "label": "testPkg.foo2",
- "kind": 10,
- "documentation": {"value": "(error) Error 2", "kind": "markdown"},
- "detail": "error name",
- "data": ["«external:file:///errorExplanationInteractive.lean»", 32, 32, 0]}
 Resolution of testPkg.foo1:
 {"textEdit":
  {"replace":
@@ -226,23 +212,24 @@ Resolution of testPkg.foo1:
  "documentation": {"value": "(error) Error 1", "kind": "markdown"},
  "detail": "error name",
  "data": ["«external:file:///errorExplanationInteractive.lean»", 32, 32, 0]}
+Resolution of testPkg.foo2:
+{"textEdit":
+ {"replace":
+  {"start": {"line": 32, "character": 23},
+   "end": {"line": 32, "character": 32}},
+  "newText": "testPkg.foo2",
+  "insert":
+  {"start": {"line": 32, "character": 23},
+   "end": {"line": 32, "character": 32}}},
+ "label": "testPkg.foo2",
+ "kind": 10,
+ "documentation": {"value": "(error) Error 2", "kind": "markdown"},
+ "detail": "error name",
+ "data": ["«external:file:///errorExplanationInteractive.lean»", 32, 32, 0]}
 {"textDocument": {"uri": "file:///errorExplanationInteractive.lean"},
  "position": {"line": 34, "character": 32}}
 {"items":
  [{"textEdit":
-   {"replace":
-    {"start": {"line": 34, "character": 23},
-     "end": {"line": 34, "character": 32}},
-    "newText": "testPkg.foo2",
-    "insert":
-    {"start": {"line": 34, "character": 23},
-     "end": {"line": 34, "character": 32}}},
-   "label": "testPkg.foo2",
-   "kind": 10,
-   "documentation": {"value": "(error) Error 2", "kind": "markdown"},
-   "detail": "error name",
-   "data": ["«external:file:///errorExplanationInteractive.lean»", 34, 32, 0]},
-  {"textEdit":
    {"replace":
     {"start": {"line": 34, "character": 23},
      "end": {"line": 34, "character": 32}},
@@ -254,22 +241,21 @@ Resolution of testPkg.foo1:
    "kind": 10,
    "documentation": {"value": "(error) Error 1", "kind": "markdown"},
    "detail": "error name",
+   "data": ["«external:file:///errorExplanationInteractive.lean»", 34, 32, 0]},
+  {"textEdit":
+   {"replace":
+    {"start": {"line": 34, "character": 23},
+     "end": {"line": 34, "character": 32}},
+    "newText": "testPkg.foo2",
+    "insert":
+    {"start": {"line": 34, "character": 23},
+     "end": {"line": 34, "character": 32}}},
+   "label": "testPkg.foo2",
+   "kind": 10,
+   "documentation": {"value": "(error) Error 2", "kind": "markdown"},
+   "detail": "error name",
    "data": ["«external:file:///errorExplanationInteractive.lean»", 34, 32, 0]}],
  "isIncomplete": false}
-Resolution of testPkg.foo2:
-{"textEdit":
- {"replace":
-  {"start": {"line": 34, "character": 23},
-   "end": {"line": 34, "character": 32}},
-  "newText": "testPkg.foo2",
-  "insert":
-  {"start": {"line": 34, "character": 23},
-   "end": {"line": 34, "character": 32}}},
- "label": "testPkg.foo2",
- "kind": 10,
- "documentation": {"value": "(error) Error 2", "kind": "markdown"},
- "detail": "error name",
- "data": ["«external:file:///errorExplanationInteractive.lean»", 34, 32, 0]}
 Resolution of testPkg.foo1:
 {"textEdit":
  {"replace":
@@ -284,6 +270,20 @@ Resolution of testPkg.foo1:
  "documentation": {"value": "(error) Error 1", "kind": "markdown"},
  "detail": "error name",
  "data": ["«external:file:///errorExplanationInteractive.lean»", 34, 32, 0]}
+Resolution of testPkg.foo2:
+{"textEdit":
+ {"replace":
+  {"start": {"line": 34, "character": 23},
+   "end": {"line": 34, "character": 32}},
+  "newText": "testPkg.foo2",
+  "insert":
+  {"start": {"line": 34, "character": 23},
+   "end": {"line": 34, "character": 32}}},
+ "label": "testPkg.foo2",
+ "kind": 10,
+ "documentation": {"value": "(error) Error 2", "kind": "markdown"},
+ "detail": "error name",
+ "data": ["«external:file:///errorExplanationInteractive.lean»", 34, 32, 0]}
 {"textDocument": {"uri": "file:///errorExplanationInteractive.lean"},
  "position": {"line": 37, "character": 31}}
 {"range":

tests/lean/run/errorExplanationLinting.lean

@@ -8,7 +8,7 @@ command.
 
 open Lean Meta
 
-/-- error: Example 'Bar' is malformed: Expected a(n) `output` code block -/
+
 #guard_msgs in
 /--
 # Examples
@@ -24,14 +24,11 @@ open Lean Meta
 ```lean broken
 ```
 -/
-register_error_explanation Lean.Example {
+register_error_explanation Lean.Example2 {
   summary := ""
   sinceVersion := ""
 }
 
-/--
-error: Example 'Foo' is malformed: Expected a(n) `output` code block, but found a(n) `lean` one
--/
 #guard_msgs in
 /--
 Foo
@@ -43,27 +40,23 @@ Foo
 ```lean fixed
 ```
 -/
-register_error_explanation Lean.Example {
+register_error_explanation Lean.Example3 {
   summary := ""
   sinceVersion := ""
 }
 
-/-- error: Expected level-2 header for an example section, but found `# End of Examples` -/
 #guard_msgs in
 /--
 # Examples
 
 # End of Examples
 -/
-register_error_explanation Lean.Example {
+register_error_explanation Lean.Example4 {
   summary := ""
   sinceVersion := ""
 }
 
 
-/--
-error: Example 'Example' is malformed: Expected a(n) broken `lean` code block, but found a(n) fixed `lean` one
--/
 #guard_msgs in
 /--
 # Examples
@@ -77,14 +70,11 @@ error: Example 'Example' is malformed: Expected a(n) broken `lean` code block, b
 ```lean broken
 ```
 -/
-register_error_explanation Lean.Example {
+register_error_explanation Lean.Example5 {
   summary := ""
   sinceVersion := ""
 }
 
-/--
-error: Example 'Example' is malformed: Expected a(n) `output` code block, but found a(n) `lean` one
--/
 #guard_msgs in
 /--
 # Examples
@@ -100,12 +90,11 @@ error: Example 'Example' is malformed: Expected a(n) `output` code block, but fo
 ```lean fixed
 ```
 -/
-register_error_explanation Lean.Example {
+register_error_explanation Lean.Example6 {
   summary := ""
   sinceVersion := ""
 }
 
-/-- error: Example 'Example' is malformed: Expected a(n) fixed `lean` code block -/
 #guard_msgs in
 /--
 # Examples
@@ -120,14 +109,11 @@ register_error_explanation Lean.Example {
 ```lean fixed
 ```
 -/
-register_error_explanation Lean.Example {
+register_error_explanation Lean.Example7 {
   summary := ""
   sinceVersion := ""
 }
 
-/--
-error: Example 'Example' is malformed: Invalid code block info string `lean broken_or_fixed`: offset 20: Invalid attribute `broken_or_fixed`
--/
 #guard_msgs in
 /--
 # Examples
@@ -141,13 +127,12 @@ error: Example 'Example' is malformed: Invalid code block info string `lean brok
 ```lean fixed
 ```
 -/
-register_error_explanation Lean.Example {
+register_error_explanation Lean.Example8 {
   summary := ""
   sinceVersion := ""
 }
 
 
-/-- error: Expected level-2 header for an example section, but found `# Examples` -/
 #guard_msgs in
 /--
 This is an explanation.
@@ -166,12 +151,11 @@ This is an explanation.
 
 Should fail
 -/
-register_error_explanation Lean.Example {
+register_error_explanation Lean.Example9 {
   summary := ""
   sinceVersion := ""
 }
 
-/-- error: Expected level-2 header for an example section, but found `# New Section` -/
 #guard_msgs in
 /--
 Pre-example
@@ -214,7 +198,7 @@ Explanation of second example.
 
 Foo
 -/
-register_error_explanation Lean.Example {
+register_error_explanation Lean.ExampleA {
   summary := ""
   sinceVersion := ""
 }