fix: show builtin syntax kind docs for antiquotation kinds

src/Init/Notation.lean

@@ -20,67 +20,70 @@ meta structure Parser.Category
 
 namespace Parser.Category
 
-/-- `command` is the syntax category for things that appear at the top level
-of a lean file. For example, `def foo := 1` is a `command`, as is
-`namespace Foo` and `end Foo`. Commands generally have an effect on the state of
-adding something to the environment (like a new definition), as well as
-commands like `variable` which modify future commands within a scope. -/
+/-- `command` is the syntax category for top-level constructs in a Lean file.
+Examples include `def foo := 1`, `theorem`, `#check`, `#eval`, `namespace Foo`,
+`open`, and `end Foo`. Commands typically update the environment (e.g., add
+declarations) or modify parsing/elaboration context for later commands (e.g.,
+`variable` or `set_option`). -/
 meta def command : Category := {}
 
-/-- `term` is the builtin syntax category for terms. A term denotes an expression
-in lean's type theory, for example `2 + 2` is a term. The difference between
-`Term` and `Expr` is that the former is a kind of syntax, while the latter is
-the result of elaboration. For example `by simp` is also a `Term`, but it elaborates
-to different `Expr`s depending on the context. -/
+/-- `term` is the builtin syntax category for terms, i.e. expressions in Lean's
+type theory. For example, `2 + 2` is a term. `Term` is syntax, while `Expr` is
+the elaborated result. A term like `by simp` elaborates differently depending on
+the surrounding expected type. This is the category referenced by `term` in
+parser DSLs such as `syntax term:60` declarations. -/
 meta def term : Category := {}
 
-/-- `tactic` is the builtin syntax category for tactics. These appear after
-`by` in proofs, and they are programs that take in the proof context
-(the hypotheses in scope plus the type of the term to synthesize) and construct
-a term of the expected type. For example, `simp` is a tactic, used in:
+/-- `tactic` is the builtin syntax category for tactics. These appear after `by`
+in proofs and are programs that transform a goal state into a proof term. The
+category underlies the tactic sequences accepted by `by` blocks and `tactic`
+declarations.
+For example, `simp` is a tactic, used in:
 ```
 example : 2 + 2 = 4 := by simp
 ```
 -/
 meta def tactic : Category := {}
 
-/-- `doElem` is a builtin syntax category for elements that can appear in the `do` notation.
-For example, `let x ← e` is a `doElem`, and a `do` block consists of a list of `doElem`s. -/
+/-- `doElem` is the builtin syntax category for elements that can appear in `do` notation.
+For example, `let x ← e`, `if ... then ... else ...`, `for`, `match`, and
+`return` are `doElem`s. A `do` block is a list of `doElem`s. -/
 meta def doElem : Category := {}
 
-/-- `structInstFieldDecl` is the syntax category for value declarations for fields in structure instance notation.
-For example, the `:= 1` and `| 0 => 0 | n + 1 => n` in `{ x := 1, f | 0 => 0 | n + 1 => n }` are in the `structInstFieldDecl` class. -/
+/-- `structInstFieldDecl` is the syntax category for field values in structure instance notation.
+For example, the `:= 1` and `| 0 => 0 | n + 1 => n` parts in
+`{ x := 1, f | 0 => 0 | n + 1 => n }` are `structInstFieldDecl`s. -/
 meta def structInstFieldDecl : Category := {}
 
-/-- `level` is a builtin syntax category for universe levels.
-This is the `u` in `Sort u`: it can contain `max` and `imax`, addition with
-constants, and variables. -/
+/-- `level` is the builtin syntax category for universe levels. This is the `u`
+in `Sort u`: levels can contain `max`/`imax`, additions with constants, and
+level variables. -/
 meta def level : Category := {}
 
-/-- `attr` is a builtin syntax category for attributes.
-Declarations can be annotated with attributes using the `@[...]` notation. -/
+/-- `attr` is the builtin syntax category for attributes.
+Declarations can be annotated with attributes using the `@[ ... ]` notation,
+e.g. `@[simp]` or `@[simp, reducible]`, and the `attribute` command parses this
+category too. -/
 meta def attr : Category := {}
 
-/-- `stx` is a builtin syntax category for syntax. This is the abbreviated
-parser notation used inside `syntax` and `macro` declarations. -/
+/-- `stx` is the builtin syntax category for the syntax DSL used inside
+`syntax`/`macro` declarations (e.g., `term:60`, string literals, `ident`,
+`sepBy`, `many`, `optional`, `indent`, `colGt`, etc.). -/
 meta def stx : Category := {}
 
-/-- `prio` is a builtin syntax category for priorities.
-Priorities are used in many different attributes.
-Higher numbers denote higher priority, and for example typeclass search will
-try high priority instances before low priority.
-In addition to literals like `37`, you can also use `low`, `mid`, `high`, as well as
-add and subtract priorities. -/
+/-- `prio` is a builtin syntax category for priorities. Higher numbers denote
+higher priority (e.g., typeclass search tries higher priorities first).
+In addition to numeric literals like `37`, you can use `default`, `low`, `mid`,
+`high`, and `+`/`-` to offset priorities. -/
 meta def prio : Category := {}
 
-/-- `prec` is a builtin syntax category for precedences. A precedence is a value
-that expresses how tightly a piece of syntax binds: for example `1 + 2 * 3` is
-parsed as `1 + (2 * 3)` because `*` has a higher precedence than `+`.
-Higher numbers denote higher precedence.
-In addition to literals like `37`, there are some special named precedence levels:
-* `arg` for the precedence of function arguments
-* `max` for the highest precedence used in term parsers (not actually the maximum possible value)
-* `lead` for the precedence of terms not supposed to be used as arguments
+/-- `prec` is a builtin syntax category for precedences. Precedence expresses how
+tightly syntax binds: `1 + 2 * 3` parses as `1 + (2 * 3)` because `*` has higher
+precedence than `+`. Higher numbers denote higher precedence.
+Besides numeric literals, there are named levels:
+* `arg` for function arguments
+* `max` for the highest precedence used in term parsers (not the maximum possible)
+* `lead` for terms not meant as arguments
 and you can also add and subtract precedences. -/
 meta def prec : Category := {}
 

src/Init/Prelude.lean

@@ -4979,25 +4979,27 @@ instance : Inhabited (TSyntax ks) where
 /-! # Builtin kinds -/
 
 /--
-The `` `choice `` kind is used to represent ambiguous parse results.
+The `` `choice `` kind represents ambiguous parse results.
 
 The parser prioritizes longer matches over shorter ones, but there is not always a unique longest
-match. All the parse results are saved, and the determination of which to use is deferred
-until typing information is available.
+match. All the parse results are saved as children of a `Syntax.node` of kind `choice` (one child
+per alternative), and the determination of which alternative to use is deferred until typing
+information is available.
 -/
 abbrev choiceKind : SyntaxNodeKind := `choice
 
 /--
-`` `null `` is the “fallback” kind, used when no other kind applies. Null nodes result from
-repetition operators, and empty null nodes represent the failure of an optional parse.
-
-The null kind is used for raw list parsers like `many`.
+`` `null `` is the “fallback” kind used for list-like parser results. Null nodes result from
+repetition operators such as `optional`, `many`, and `sepBy`. An empty null node represents the
+failure of an optional parse, and a nonempty null node collects the parsed items in order.
 -/
 abbrev nullKind : SyntaxNodeKind := `null
 
 /--
-The `` `group `` kind is used for nodes that result from `Lean.Parser.group`. This avoids confusion
-with the null kind when used inside `optional`.
+The `` `group `` kind is used for nodes that result from `Lean.Parser.group`. Grouping ensures that
+parsers with arity greater than 1 are wrapped to produce a single node, which prevents list
+combinators such as `optional` and `many` from conflating a parsed value with an empty `null` node.
+For example, `many(p)` stores each iteration as a single child node even if `p` itself has arity > 1.
 -/
 abbrev groupKind : SyntaxNodeKind := `group
 
@@ -5032,7 +5034,11 @@ abbrev scientificLitKind : SyntaxNodeKind := `scientific
 /-- `` `name `` is the node kind of name literals like `` `foo ``. -/
 abbrev nameLitKind : SyntaxNodeKind := `name
 
-/-- `` `fieldIdx `` is the node kind of projection indices like the `2` in `x.2`. -/
+/--
+`` `fieldIdx `` is the node kind of numeric projection indices like the `2` in `x.2`.
+These are positive decimal indices without a leading zero, used both in projection notation and in
+structure instance field paths (e.g. `{ x.2 := ... }`).
+-/
 abbrev fieldIdxKind : SyntaxNodeKind := `fieldIdx
 
 /--
@@ -5041,18 +5047,23 @@ abbrev fieldIdxKind : SyntaxNodeKind := `fieldIdx
 anything.
 
 They can be used to generate identifiers (with `Lean.HygieneInfo.mkIdent`) as if they were
-introduced in a macro's input, rather than by its implementation.
+introduced in a macro's input, rather than by its implementation. The node has a single child,
+an anonymous `Syntax.ident` whose macro scopes record the hygiene context.
 -/
 abbrev hygieneInfoKind : SyntaxNodeKind := `hygieneInfo
 
 /--
-`` `interpolatedStrLitKind `` is the node kind of interpolated string literal
-fragments like `"value = {` and `}"` in `s!"value = {x}"`.
+`` `interpolatedStrLitKind `` is the node kind of literal fragments inside an interpolated string.
+For example, in `s!"value = {x}"`, the fragments `"value = {` and `}"` are `interpolatedStrLitKind`
+nodes, and they alternate with the parsed `{...}` holes. These fragments are raw substrings of the
+original literal (escapes are not interpreted here).
 -/
 abbrev interpolatedStrLitKind : SyntaxNodeKind := `interpolatedStrLitKind
 /--
-`` `interpolatedStrKind `` is the node kind of an interpolated string literal like `"value = {x}"`
-in `s!"value = {x}"`.
+`` `interpolatedStrKind `` is the node kind of an interpolated string literal like `s!"value = {x}"`.
+The node has an odd number of arguments, alternating between literal fragments (of kind
+`interpolatedStrLitKind`) and the parsed holes. For example, `"foo\n{2 + 2}"` yields three children:
+the literal fragment `"foo\n{`, the parsed term `2 + 2`, and the fragment `}"`.
 -/
 abbrev interpolatedStrKind : SyntaxNodeKind := `interpolatedStrKind
 

src/Lean/Elab/Quotation.lean

@@ -108,14 +108,42 @@ def mkNode (b : ArrayStxBuilder) (k : SyntaxNodeKind) : TermElabM Term := do
 
 end ArrayStxBuilder
 
+private def builtinSyntaxNodeKindDecl? (k : SyntaxNodeKind) : Option Name :=
+  match k with
+  | `choice => some ``Lean.choiceKind
+  | `null => some ``Lean.nullKind
+  | `group => some ``Lean.groupKind
+  | `ident => some ``Lean.identKind
+  | `str => some ``Lean.strLitKind
+  | `char => some ``Lean.charLitKind
+  | `num => some ``Lean.numLitKind
+  | `hexnum => some ``Lean.hexnumKind
+  | `scientific => some ``Lean.scientificLitKind
+  | `name => some ``Lean.nameLitKind
+  | `fieldIdx => some ``Lean.fieldIdxKind
+  | `hygieneInfo => some ``Lean.hygieneInfoKind
+  | `interpolatedStrLitKind => some ``Lean.interpolatedStrLitKind
+  | `interpolatedStrKind => some ``Lean.interpolatedStrKind
+  | _ => none
+
+private def antiquotKindName? (stx : Syntax) : Option Name :=
+  match stx with
+  | Syntax.ident _ _ val _ => some val
+  | Syntax.atom _ val => some (Name.mkSimple val)
+  | _ => none
+
 def tryAddSyntaxNodeKindInfo (stx : Syntax) (k : SyntaxNodeKind) : TermElabM Unit := do
-  if (← getEnv).contains k then
+  let env ← getEnv
+  if env.contains k then
     addTermInfo' stx (← mkConstWithFreshMVarLevels k)
   else
     -- HACK to support built in categories, which use a different naming convention
-    let k := ``Lean.Parser.Category ++ k
-    if (← getEnv).contains k then
-      addTermInfo' stx (← mkConstWithFreshMVarLevels k)
+    let catName := ``Lean.Parser.Category ++ k
+    if env.contains catName then
+      addTermInfo' stx (← mkConstWithFreshMVarLevels catName)
+    else if let some declName := builtinSyntaxNodeKindDecl? k then
+      if env.contains declName then
+        addTermInfo' stx (← mkConstWithFreshMVarLevels declName)
 
 instance : Quote Syntax.Preresolved where
   quote
@@ -145,7 +173,10 @@ private partial def quoteSyntax : Syntax → TermElabM Term
   | stx@(Syntax.node _ k _) => do
     if let some (k, _) := stx.antiquotKind? then
       if let some name := getAntiquotKindSpec? stx then
-        tryAddSyntaxNodeKindInfo name k
+        if let some kindName := antiquotKindName? name then
+          tryAddSyntaxNodeKindInfo name kindName
+        else
+          tryAddSyntaxNodeKindInfo name k
     if isAntiquots stx && !isEscapedAntiquot (getCanonicalAntiquot stx) then
       let ks := antiquotKinds stx
       `(@TSyntax.raw $(quote <| ks.map (·.1)) $(getAntiquotTerm (getCanonicalAntiquot stx)))
@@ -350,7 +381,10 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
     let quoted := getQuotContent pat
     if let some (k, _) := quoted.antiquotKind? then
       if let some name := getAntiquotKindSpec? quoted then
-        tryAddSyntaxNodeKindInfo name k
+        if let some kindName := antiquotKindName? name then
+          tryAddSyntaxNodeKindInfo name kindName
+        else
+          tryAddSyntaxNodeKindInfo name k
     if quoted.isAtom || quoted.isOfKind `patternIgnore then
       -- We assume that atoms are uniquely determined by the node kind and never have to be checked
       unconditionally pure

src/Lean/Parser/Attr.lean

@@ -30,6 +30,7 @@ attribute [run_builtin_parser_attribute_hooks]
   priorityParser attrParser
 
 namespace Priority
+/-- Numeric literal for attribute priorities. -/
 @[builtin_prio_parser] def numPrio  := checkPrec maxPrec >> numLit
 attribute [run_builtin_parser_attribute_hooks] numPrio
 end Priority

src/Lean/Parser/Command.lean

@@ -18,7 +18,7 @@ namespace Parser
 /-- Syntax quotation for terms. -/
 @[builtin_term_parser] def Term.quot := leading_parser
   "`(" >> withoutPosition (incQuotDepth termParser) >> ")"
-@[builtin_term_parser] def Term.precheckedQuot := leading_parser
+@[inherit_doc Term.quot, builtin_term_parser] def Term.precheckedQuot := leading_parser
   "`" >> Term.quot
 
 namespace Command
@@ -280,6 +280,7 @@ def «structure»          := leading_parser
   declModifiers false >>
   («abbrev» <|> definition <|> «theorem» <|> «opaque» <|> «instance» <|> «axiom» <|> «example» <|>
    «inductive» <|> «coinductive» <|> classInductive <|> «structure»)
+/-- `deriving instance` declares typeclass instances to be generated for a declaration. -/
 @[builtin_command_parser] def «deriving»     := leading_parser
   "deriving " >> "instance " >> derivingClasses >> " for " >> sepBy1 (recover termParser skip) ", "
 def sectionHeader := leading_parser
@@ -526,8 +527,10 @@ structure Pair (α : Type u) (β : Type v) : Type (max u v) where
 -/
 @[builtin_command_parser] def «universe»     := leading_parser
   "universe" >> many1 (ppSpace >> checkColGt >> ident)
+/-- `#check e` reports the type of `e`, printing `e : T`. -/
 @[builtin_command_parser] def check          := leading_parser
   "#check " >> termParser
+/-- Like `#check`, but succeeds only if `e` fails to type check. -/
 @[builtin_command_parser] def check_failure  := leading_parser
   "#check_failure " >> termParser -- Like `#check`, but succeeds only if term does not type check
 /--
@@ -558,16 +561,22 @@ See also: `#reduce e` for evaluation by term reduction.
   "#eval " >> termParser
 @[builtin_command_parser, inherit_doc eval] def evalBang := leading_parser
   "#eval! " >> termParser
+/-- `#synth T` tries to synthesize a typeclass instance of type `T` and prints the result. -/
 @[builtin_command_parser] def synth          := leading_parser
   "#synth " >> termParser
+/-- Debugging command that logs a warning and interrupts processing after this point. -/
 @[builtin_command_parser] def exit           := leading_parser
   "#exit"
+/-- `#print n` prints the declaration `n`; `#print "msg"` prints the string literal contents. -/
 @[builtin_command_parser] def print          := leading_parser
   "#print " >> (ident <|> strLit)
+/-- `#print sig n` prints only the signature of `n`. -/
 @[builtin_command_parser] def printSig       := leading_parser
   "#print " >> nonReservedSymbol "sig " >> ident
+/-- `#print axioms n` prints the axioms that `n` depends on. -/
 @[builtin_command_parser] def printAxioms    := leading_parser
   "#print " >> nonReservedSymbol "axioms " >> ident
+/-- `#print equations n` prints the definitional equations for `n`, if any. -/
 @[builtin_command_parser] def printEqns      := leading_parser
   "#print " >> (nonReservedSymbol "equations " <|> nonReservedSymbol "eqns ") >> ident
 /--
@@ -576,7 +585,7 @@ Displays all available tactic tags, with documentation.
 @[builtin_command_parser] def printTacTags   := leading_parser
   "#print " >> nonReservedSymbol "tactic " >> nonReservedSymbol "tags"
 /--
-`#where` gives a description of the state of the current scope scope.
+`#where` gives a description of the state of the current scope.
 This includes the current namespace, `open` namespaces, `universe` and `variable` commands,
 and options set with `set_option`.
 -/
@@ -622,6 +631,7 @@ only in a single term or tactic.
   "set_option " >> identWithPartialTrailingDot >> ppSpace >> optionValue
 def eraseAttr := leading_parser
   "-" >> rawIdent
+/-- Applies attributes to the listed declarations. -/
 @[builtin_command_parser] def «attribute»    := leading_parser
   "attribute " >> "[" >>
     withoutPosition (sepBy1 (eraseAttr <|> Term.attrInstance) ", ") >>
@@ -785,15 +795,18 @@ end
 @[builtin_command_parser] def «open»    := leading_parser
   withPosition ("open" >> openDecl)
 
+/-- Groups mutually recursive commands in a `mutual ... end` block. -/
 @[builtin_command_parser] def «mutual» := leading_parser
   "mutual" >> many1 (ppLine >> notSymbol "end" >> commandParser) >>
   ppDedent (ppLine >> "end")
 def initializeKeyword := leading_parser
   "initialize " <|> "builtin_initialize "
+/-- Declares initialization code to run when a module is loaded. -/
 @[builtin_command_parser] def «initialize» := leading_parser
   declModifiers false >> initializeKeyword >>
   optional (atomic (ident >> Term.typeSpec >> ppSpace >> Term.leftArrow)) >> Term.doSeq
 
+/-- Scopes a single command under a preceding `... in` construct. -/
 @[builtin_command_parser] def «in»  := trailing_parser
   withOpen (ppDedent (" in" >> ppLine >> commandParser))
 

src/Lean/Parser/Level.lean

@@ -21,18 +21,23 @@ builtin_initialize
 
 namespace Level
 
+/-- Parenthesized universe level, e.g. `(u)` or `(max u v)`. -/
 @[builtin_level_parser] def paren  := leading_parser
   "(" >> withoutPosition levelParser >> ")"
+/-- `max`-combinations of universe levels, e.g. `max u v`. -/
 @[builtin_level_parser] def max    := leading_parser
   nonReservedSymbol "max" true  >> many1 (ppSpace >> levelParser maxPrec)
+/-- `imax`-combinations of universe levels, e.g. `imax u v`. -/
 @[builtin_level_parser] def imax   := leading_parser
   nonReservedSymbol "imax" true >> many1 (ppSpace >> levelParser maxPrec)
+/-- Hole for a universe level. -/
 @[builtin_level_parser] def hole   := leading_parser
   "_"
-@[builtin_level_parser] def num    :=
+@[inherit_doc Lean.Parser.numLit, builtin_level_parser] def num    :=
   checkPrec maxPrec >> numLit
-@[builtin_level_parser] def ident  :=
+@[inherit_doc Lean.Parser.ident, builtin_level_parser] def ident  :=
   checkPrec maxPrec >> Parser.ident
+/-- Addition of a numeric literal to a universe level, e.g. `u + 1`. -/
 @[builtin_level_parser] def addLit := trailing_parser:65
   " + " >> numLit