diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index cdfcc1386b8d..43da1760bf30 100644
--- a/src/Init/Notation.lean
+++ b/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 := {}
 
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index ee41f63e208b..555bc7ce3eaf 100644
--- a/src/Init/Prelude.lean
+++ b/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
 
diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean
index a6c817a4c670..8620e5d75935 100644
--- a/src/Lean/Elab/Quotation.lean
+++ b/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
diff --git a/src/Lean/Parser/Attr.lean b/src/Lean/Parser/Attr.lean
index f5cac7a9a464..3b3605a0a31b 100644
--- a/src/Lean/Parser/Attr.lean
+++ b/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
diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index 35f5c2057a2b..114024794571 100644
--- a/src/Lean/Parser/Command.lean
+++ b/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))
 
diff --git a/src/Lean/Parser/Level.lean b/src/Lean/Parser/Level.lean
index 7f3e1d1224f7..6c4bd1af5fc5 100644
--- a/src/Lean/Parser/Level.lean
+++ b/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
 
diff --git a/src/Lean/Parser/Syntax.lean b/src/Lean/Parser/Syntax.lean
index 56e98db3c6f4..10dd2d6c6d84 100644
--- a/src/Lean/Parser/Syntax.lean
+++ b/src/Lean/Parser/Syntax.lean
@@ -32,19 +32,29 @@ def «precedence» := leading_parser
 def optPrecedence := optional (atomic «precedence»)
 
 namespace Syntax
+/-! Parsers for the `syntax` DSL itself. -/
+-- Keep docs short; these are primarily for hover/help in editors.
+
+/-- Numeric literal for precedence expressions. -/
 @[builtin_prec_parser] def numPrec := checkPrec maxPrec >> numLit
 
+/-- Parenthesized syntax DSL expression, used for grouping. -/
 @[builtin_syntax_parser] def paren           := leading_parser
   "(" >> withoutPosition (many1 syntaxParser) >> ")"
+/-- Reference to a parser category or alias, optionally with precedence (e.g. `term` or `term:60`). -/
 @[builtin_syntax_parser] def cat             := leading_parser
   ident >> optPrecedence
+/-- Syntax DSL form `f(p)` for a unary parser alias. -/
 @[builtin_syntax_parser] def unary           := leading_parser
   ident >> checkNoWsBefore >> "(" >> withoutPosition (many1 syntaxParser) >> ")"
+/-- Syntax DSL form `f(p, q)` for a binary parser alias. -/
 @[builtin_syntax_parser] def binary          := leading_parser
   ident >> checkNoWsBefore >> "(" >> withoutPosition (many1 syntaxParser >> ", " >> many1 syntaxParser) >> ")"
+/-- Syntax DSL `sepBy(p, sep[, psep][, allowTrailingSep])` list parser. -/
 @[builtin_syntax_parser] def sepBy           := leading_parser
   "sepBy(" >> withoutPosition (many1 syntaxParser >> ", " >> strLit >>
     optional (", " >> many1 syntaxParser) >> optional (", " >> nonReservedSymbol "allowTrailingSep")) >> ")"
+/-- Nonempty list variant of `sepBy`. -/
 @[builtin_syntax_parser] def sepBy1          := leading_parser
   "sepBy1(" >> withoutPosition (many1 syntaxParser >> ", " >> strLit >>
     optional (", " >> many1 syntaxParser) >> optional (", " >> nonReservedSymbol "allowTrailingSep")) >> ")"
@@ -89,9 +99,11 @@ def «infixr»   := leading_parser "infixr"
 -/
 def «postfix»  := leading_parser "postfix"
 def mixfixKind := «prefix» <|> «infix» <|> «infixl» <|> «infixr» <|> «postfix»
+/-- Declare a `prefix`/`infix`/`postfix` notation. -/
 @[builtin_command_parser] def «mixfix»   := leading_parser
   optional docComment >> optional Term.«attributes» >> Term.attrKind >> mixfixKind >>
   precedence >> optNamedName >> optNamedPrio >> ppSpace >> notationItem >> darrow >> termParser
+/-- Declare a general notation. -/
 @[builtin_command_parser] def «notation»    := leading_parser
   optional docComment >> optional Term.«attributes» >> Term.attrKind >>
   "notation" >> optPrecedence >> optNamedName >> optNamedPrio >> many (ppSpace >> notationItem) >> darrow >> termParser
@@ -99,31 +111,40 @@ def mixfixKind := «prefix» <|> «infix» <|> «infixl» <|> «infixr» <|> «p
 -- NOTE: We use `suppressInsideQuot` in the following parsers because quotations inside them are evaluated in the same stage and
 -- thus should be ignored when we use `checkInsideQuot` to prepare the next stage for a builtin syntax change
 def optKind : Parser := optional (" (" >> nonReservedSymbol "kind" >> ":=" >> ident >> ")")
+/-- Declare a family of macros by pattern (use `(kind := ...)` to disambiguate). -/
 @[builtin_command_parser] def «macro_rules» := suppressInsideQuot <| leading_parser
   optional docComment >> optional Term.«attributes» >> Term.attrKind >>
   "macro_rules" >> optKind >> Term.matchAlts
+/-- Declare new syntax in a category, with optional precedence, name, and priority.
+If the precedence is omitted, atom-like syntax defaults to `maxPrec` and other syntax to `leadPrec`.
+If `name :=` is omitted, a name is generated from the syntax. -/
 @[builtin_command_parser] def «syntax»      := leading_parser
   optional docComment >> optional Term.«attributes» >> Term.attrKind >>
   "syntax " >> optPrecedence >> optNamedName >> optNamedPrio >> many1 (ppSpace >> syntaxParser argPrec) >> " : " >> ident
+/-- Declare a reusable syntax abbreviation `syntax <name> := ...` (no category), for use in other syntax rules. -/
 @[builtin_command_parser] def syntaxAbbrev  := leading_parser
   optional docComment >> optional visibility >> "syntax " >> ident >> " := " >> many1 syntaxParser
 def catBehaviorBoth   := leading_parser nonReservedSymbol "both"
 def catBehaviorSymbol := leading_parser nonReservedSymbol "symbol"
 def catBehavior := optional (" (" >> nonReservedSymbol "behavior" >> " := " >> (catBehaviorBoth <|> catBehaviorSymbol) >> ")")
+/-- Declare a new syntax category. -/
 @[builtin_command_parser] def syntaxCat := leading_parser
   optional docComment >> "declare_syntax_cat " >> ident >> catBehavior
 def macroArg  := leading_parser
   optional (atomic (ident >> checkNoWsBefore "no space before ':'" >> ":")) >> syntaxParser argPrec
 def macroRhs : Parser := leading_parser withPosition termParser
 def macroTail := leading_parser atomic (" : " >> ident) >> darrow >> macroRhs
+/-- Declare a single macro with explicit arguments and expansion. -/
 @[builtin_command_parser] def «macro»       := leading_parser suppressInsideQuot <|
   optional docComment >> optional Term.«attributes» >> Term.attrKind >>
   "macro" >> optPrecedence >> optNamedName >> optNamedPrio >> many1 (ppSpace >> macroArg) >> macroTail
+/-- Declare elaborator rules for syntax (use `(kind := ...)` to disambiguate). -/
 @[builtin_command_parser] def «elab_rules» := leading_parser suppressInsideQuot <|
   optional docComment >> optional Term.«attributes» >> Term.attrKind >>
   "elab_rules" >> optKind >> optional (" : " >> ident) >> optional (" <= " >> ident) >> Term.matchAlts
 def elabArg  := macroArg
 def elabTail := leading_parser atomic (" : " >> ident >> optional (" <= " >> ident)) >> darrow >> withPosition termParser
+/-- Declare a single elaborator for syntax. -/
 @[builtin_command_parser] def «elab»       := leading_parser suppressInsideQuot <|
   optional docComment >> optional Term.«attributes» >> Term.attrKind >>
   "elab" >> optPrecedence >> optNamedName >> optNamedPrio >> many1 (ppSpace >> elabArg) >> elabTail
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 5c3d8e1b7011..c6f65a9a06a4 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -121,15 +121,15 @@ def optSemicolon (p : Parser) : Parser :=
   ppDedent $ semicolonOrLinebreak >> ppLine >> p
 
 -- `checkPrec` necessary for the pretty printer
-@[builtin_term_parser] def ident :=
+@[inherit_doc Lean.Parser.ident, builtin_term_parser] def ident :=
   checkPrec maxPrec >> Parser.ident
-@[builtin_term_parser] def num : Parser :=
+@[inherit_doc Lean.Parser.numLit, builtin_term_parser] def num : Parser :=
   checkPrec maxPrec >> numLit
-@[builtin_term_parser] def scientific : Parser :=
+@[inherit_doc Lean.Parser.scientificLit, builtin_term_parser] def scientific : Parser :=
   checkPrec maxPrec >> scientificLit
-@[builtin_term_parser] def str : Parser :=
+@[inherit_doc Lean.Parser.strLit, builtin_term_parser] def str : Parser :=
   checkPrec maxPrec >> strLit
-@[builtin_term_parser] def char : Parser :=
+@[inherit_doc Lean.Parser.charLit, builtin_term_parser] def char : Parser :=
   checkPrec maxPrec >> charLit
 /-- A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. -/
 @[builtin_term_parser] def type := leading_parser
diff --git a/tests/lean/run/hover_builtin_syntax_kinds.lean b/tests/lean/run/hover_builtin_syntax_kinds.lean
new file mode 100644
index 000000000000..88b71e0f96fd
--- /dev/null
+++ b/tests/lean/run/hover_builtin_syntax_kinds.lean
@@ -0,0 +1,33 @@
+import Lean
+open Lean
+
+set_option guard_msgs.diff false
+
+#info_trees in
+def miscQuot : MacroM (TSyntax `term) := do
+  let numStx : TSyntax `num := Syntax.mkNumLit "1"
+  let identStx : TSyntax `ident := mkIdent `foo
+  let strStx : TSyntax `str := Syntax.mkStrLit "hi"
+  let charStx : TSyntax `char := Syntax.mkCharLit 'A'
+  let sciStx : TSyntax `scientific := Syntax.mkScientificLit "1.2e3"
+  let nameStx : TSyntax `name := Syntax.mkNameLit "`Foo"
+  let fieldStx : TSyntax `fieldIdx := Syntax.mkLit fieldIdxKind "2"
+  let hygieneStx : TSyntax `hygieneInfo :=
+    ⟨Syntax.node SourceInfo.none hygieneInfoKind #[mkIdent `x]⟩
+  let lit1 : Syntax := Syntax.mkLit interpolatedStrLitKind "foo{"
+  let lit2 : Syntax := Syntax.mkLit interpolatedStrLitKind "}"
+  let interp : TSyntax `interpolatedStrKind :=
+    ⟨Syntax.node SourceInfo.none interpolatedStrKind #[lit1, Syntax.mkNumLit "1", lit2]⟩
+  let hexStx : TSyntax `hexnum := Syntax.mkLit hexnumKind "ea10"
+  let e : TSyntax `term := mkIdent `x
+  let _ ← `($numStx:num)
+  let _ ← `($identStx:ident)
+  let _ ← `($strStx:str)
+  let _ ← `($charStx:char)
+  let _ ← `($sciStx:scientific)
+  let _ ← `($nameStx:name)
+  let _ ← `($e.$fieldStx:fieldIdx)
+  let _ ← `(($hygieneStx:hygieneInfo $e))
+  let _ ← `(throwError $interp:interpolatedStr)
+  let _ ← `(Parser.Tactic.grindParam| #$hexStx:hexnum)
+  return (← `($e))