diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index c32a34a0fe..378340ca4c 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -1396,12 +1396,9 @@ private def elabAtom : TermElab := fun stx expectedType? => do
   annotateIfRec stx (← elabAppAux stx #[] #[] (ellipsis := false) expectedType?)
 
 @[builtinTermElab ident] def elabIdent : TermElab := elabAtom
-/-- `x@e` matches the pattern `e` and binds its value to the identifier `x`. -/
 @[builtinTermElab namedPattern] def elabNamedPattern : TermElab := elabAtom
 @[builtinTermElab dotIdent] def elabDotIdent : TermElab := elabAtom
-/-- `x.{u, ...}` explicitly specifies the universes `u, ...` of the constant `x`. -/
 @[builtinTermElab explicitUniv] def elabExplicitUniv : TermElab := elabAtom
-/-- `e |>.x` is a shorthand for `(e).x`. It is especially useful for avoiding parentheses with repeated applications. -/
 @[builtinTermElab pipeProj] def elabPipeProj : TermElab
   | `($e |>.$f $args*), expectedType? =>
     universeConstraintsCheckpoint do
@@ -1409,9 +1406,6 @@ private def elabAtom : TermElab := fun stx expectedType? => do
       elabAppAux (← `($e |>.$f)) namedArgs args (ellipsis := ellipsis) expectedType?
   | _, _ => throwUnsupportedSyntax
 
-/--
-`@x` disables automatic insertion of implicit parameters of the constant `x`.
-`@e` for any term `e` also disables the insertion of implicit lambdas at this position. -/
 @[builtinTermElab explicit] def elabExplicit : TermElab := fun stx expectedType? =>
   match stx with
   | `(@$_:ident)         => elabAtom stx expectedType?  -- Recall that `elabApp` also has support for `@`
diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index d61b686cc5..58e49bb36e 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -26,12 +26,6 @@ open Meta
       mkCoe expectedType type e
   | _ => throwError "invalid coercion notation, expected type is not known"
 
-/--
-The *anonymous constructor* `⟨e, ...⟩` is equivalent to `c e ...` if the
-expected type is an inductive type with a single constructor `c`.
-If more terms are given than `c` has parameters, the remaining arguments
-are turned into a new anonymous constructor application. For example,
-`⟨a, b, c⟩ : α × (β × γ)` is equivalent to `⟨a, ⟨b, c⟩⟩`. -/
 @[builtinTermElab anonymousCtor] def elabAnonymousCtor : TermElab := fun stx expectedType? =>
   match stx with
   | `(⟨$args,*⟩) => do
@@ -123,13 +117,6 @@ private def elabTParserMacroAux (prec lhsPrec e : Term) : TermElabM Syntax := do
     elabTParserMacroAux (prec?.getD <| quote Parser.maxPrec) (lhsPrec?.getD <| quote 0) e
   | _ => throwUnsupportedSyntax
 
-/--
-`panic! msg` formally evaluates to `@Inhabited.default α` if the expected type
-`α` implements `Inhabited`.
-At runtime, `msg` and the file position are printed to stderr unless the C
-function `lean_set_panic_messages(false)` has been executed before. If the C
-function `lean_set_exit_on_panic(true)` has been executed before, the process is
-then aborted. -/
 @[builtinTermElab Lean.Parser.Term.panic] def elabPanic : TermElab := fun stx expectedType? => do
   match stx with
   | `(panic! $arg) =>
@@ -141,11 +128,9 @@ then aborted. -/
     withMacroExpansion stx stxNew $ elabTerm stxNew expectedType?
   | _ => throwUnsupportedSyntax
 
-/-- A shorthand for `panic! "unreachable code has been reached"`. -/
 @[builtinMacro Lean.Parser.Term.unreachable]  def expandUnreachable : Macro := fun _ =>
   `(panic! "unreachable code has been reached")
 
-/-- `assert! cond` panics if `cond` evaluates to `false`. -/
 @[builtinMacro Lean.Parser.Term.assert]  def expandAssert : Macro
   | `(assert! $cond; $body) =>
     -- TODO: support for disabling runtime assertions
@@ -154,15 +139,11 @@ then aborted. -/
     | none => `(if $cond then $body else panic! ("assertion violation"))
   | _ => Macro.throwUnsupported
 
-/--
-`dbg_trace e; body` evaluates to `body` and prints `e` (which can be an
-interpolated string literal) to stderr. It should only be used for debugging. -/
 @[builtinMacro Lean.Parser.Term.dbgTrace]  def expandDbgTrace : Macro
   | `(dbg_trace $arg:interpolatedStr; $body) => `(dbgTrace (s! $arg) fun _ => $body)
   | `(dbg_trace $arg:term; $body)            => `(dbgTrace (toString $arg) fun _ => $body)
   | _                                        => Macro.throwUnsupported
 
-/-- A temporary placeholder for a missing proof or value. -/
 @[builtinTermElab «sorry»] def elabSorry : TermElab := fun stx expectedType? => do
   let stxNew ← `(sorryAx _ false)
   withMacroExpansion stx stxNew <| elabTerm stxNew expectedType?
@@ -241,19 +222,6 @@ where
     | `(($e)) => Term.expandCDot? e
     | _ => Term.expandCDot? stx
 
-
-/--
-You can use parentheses for
-- Grouping expressions, e.g., `a * (b + c)`.
-- Creating tuples, e.g., `(a, b, c)` is notation for `Prod.mk a (Prod.mk b c)`.
-- Performing type ascription, e.g., `(0 : Int)` instructs Lean to process `0` as a value of type `Int`.
-- Creating `Unit.unit`, `()` is just a shorthand for `Unit.unit`.
-- Creating simple functions when combined with `·`. Here are some examples:
-  - `(· + 1)` is shorthand for `fun x => x + 1`
-  - `(· + ·)` is shorthand for `fun x y => x + y`
-  - `(f · a b)` is shorthand for `fun x => f x a b`
-  - `(h (· + 1) ·)` is shorthand for `fun x => h (fun y => y + 1) x`
--/
 @[builtinMacro Lean.Parser.Term.paren] def expandParen : Macro
   | `(())           => `(Unit.unit)
   | `(($e : $type)) => do
@@ -298,12 +266,6 @@ private def withLocalIdentFor (stx : Term) (e : Expr) (k : Term → TermElabM Ex
     let aux ← withLocalDeclD id (← inferType e) fun x => do mkLambdaFVars #[x] (← k (mkIdentFrom stx id))
     return mkApp aux e
 
-/--
-`h ▸ e` is a macro built on top of `Eq.rec` and `Eq.symm` definitions.
-Given `h : a = b` and `e : p a`, the term `h ▸ e` has type `p b`.
-You can also view `h ▸ e` as a "type casting" operation where you change the type of `e` by using `h`.
-See the Chapter "Quantifiers and Equality" in the manual "Theorem Proving in Lean" for additional information.
--/
 @[builtinTermElab subst] def elabSubst : TermElab := fun stx expectedType? => do
   let expectedType? ← tryPostponeIfHasMVars? expectedType?
   match stx with
diff --git a/src/Lean/Elab/BuiltinTerm.lean b/src/Lean/Elab/BuiltinTerm.lean
index 9f7cc65eea..6f005ac32e 100644
--- a/src/Lean/Elab/BuiltinTerm.lean
+++ b/src/Lean/Elab/BuiltinTerm.lean
@@ -9,7 +9,6 @@ import Lean.Elab.Eval
 namespace Lean.Elab.Term
 open Meta
 
-/-- The universe of propositions. `Prop ≡ Sort 0`. -/
 @[builtinTermElab «prop»] def elabProp : TermElab := fun _ _ =>
   return mkSort levelZero
 
@@ -19,11 +18,9 @@ private def elabOptLevel (stx : Syntax) : TermElabM Level :=
   else
     elabLevel stx[0]
 
-/-- A specific universe in Lean's infinite hierarchy of universes. -/
 @[builtinTermElab «sort»] def elabSort : TermElab := fun stx _ =>
   return mkSort (← elabOptLevel stx[1])
 
-/-- A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. -/
 @[builtinTermElab «type»] def elabTypeStx : TermElab := fun stx _ =>
   return mkSort (mkLevelSucc (← elabOptLevel stx[1]))
 
@@ -56,7 +53,6 @@ private def elabOptLevel (stx : Syntax) : TermElabM Level :=
   else
     elabPipeCompletion stx expectedType?
 
-/-- A placeholder term, to be synthesized by unification. -/
 @[builtinTermElab «hole»] def elabHole : TermElab := fun stx expectedType? => do
   let mvar ← mkFreshExprMVar expectedType?
   registerMVarErrorHoleInfo mvar.mvarId! stx
@@ -149,7 +145,6 @@ private def mkTacticMVar (type : Expr) (tacticCode : Syntax) : TermElabM Expr :=
   registerSyntheticMVar ref mvarId <| SyntheticMVarKind.tactic tacticCode (← saveContext)
   return mvar
 
-/-- `by tac` constructs a term of the expected type by running the tactic(s) `tac`. -/
 @[builtinTermElab byTactic] def elabByTactic : TermElab := fun stx expectedType? => do
   match expectedType? with
   | some expectedType => mkTacticMVar expectedType stx
@@ -208,30 +203,19 @@ def elabScientificLit : TermElab := fun stx expectedType? => do
   | some val => return mkApp (Lean.mkConst ``Char.ofNat) (mkRawNatLit val.toNat)
   | none     => throwIllFormedSyntax
 
-/-- A literal of type `Name`. -/
 @[builtinTermElab quotedName] def elabQuotedName : TermElab := fun stx _ =>
   match stx[0].isNameLit? with
   | some val => pure $ toExpr val
   | none     => throwIllFormedSyntax
 
-/--
-A resolved name literal. Evaluates to the full name of the given constant if
-existent in the current context, or else fails. -/
 @[builtinTermElab doubleQuotedName] def elabDoubleQuotedName : TermElab := fun stx _ =>
   return toExpr (← resolveGlobalConstNoOverloadWithInfo stx[2])
 
-/-- A macro which evaluates to the name of the currently elaborating declaration. -/
 @[builtinTermElab declName] def elabDeclName : TermElab := adaptExpander fun _ => do
   let some declName ← getDeclName?
     | throwError "invalid `decl_name%` macro, the declaration name is not available"
   return (quote declName : Term)
 
-/--
-* `with_decl_name% id e` elaborates `e` in a context while changing the effective
-  declaration name to `id`.
-* `with_decl_name% ? id e` does the same, but resolves `id` as a new definition name
-  (appending the current namespaces).
--/
 @[builtinTermElab Parser.Term.withDeclName] def elabWithDeclName : TermElab := fun stx expectedType? => do
   let id := stx[2].getId
   let id := if stx[1].isNone then id else (← getCurrNamespace) ++ id
@@ -283,7 +267,6 @@ private def mkSilentAnnotationIfHole (e : Expr) : TermElabM Expr := do
   | none     => throwIllFormedSyntax
   | some msg => elabTermEnsuringType stx[2] expectedType? (errorMsgHeader? := msg)
 
-/-- `open ... in e` makes the given namespaces available in the term `e`. -/
 @[builtinTermElab «open»] def elabOpen : TermElab := fun stx expectedType? => do
   try
     pushScope
@@ -293,7 +276,6 @@ private def mkSilentAnnotationIfHole (e : Expr) : TermElabM Expr := do
   finally
     popScope
 
-/-- `set_option opt val in e` sets the option `opt` to the value `val` in the term `e`. -/
 @[builtinTermElab «set_option»] def elabSetOption : TermElab := fun stx expectedType? => do
   let options ← Elab.elabSetOption stx[1] stx[2]
   withTheReader Core.Context (fun ctx => { ctx with maxRecDepth := maxRecDepth.get options, options := options }) do
diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean
index 61da709e1a..35e545ec54 100644
--- a/src/Lean/Elab/Match.lean
+++ b/src/Lean/Elab/Match.lean
@@ -1245,15 +1245,6 @@ where
   isAtomicIdent (stx : Syntax) : Bool :=
     stx.isIdent && stx.getId.eraseMacroScopes.isAtomic
 
-/--
-Pattern matching. `match e, ... with | p, ... => f | ...` matches each given
-term `e` against each pattern `p` of a match alternative. When all patterns
-of an alternative match, the `match` term evaluates to the value of the
-corresponding right-hand side `f` with the pattern variables bound to the
-respective matched values.
-When not constructing a proof, `match` does not automatically substitute variables
-matched on in dependent variables' types. Use `match (generalizing := true) ...` to
-enforce this. -/
 @[builtinTermElab «match»] def elabMatch : TermElab := fun stx expectedType? => do
   match stx with
   | `(match $discr:term with | $y:ident => $rhs) =>
@@ -1277,9 +1268,6 @@ builtin_initialize
   registerTraceClass `Elab.match
 
 -- leading_parser:leadPrec "nomatch " >> termParser
-/-- Empty match/ex falso. `nomatch e` is of arbitrary type `α : Sort u` if
-Lean can show that an empty set of patterns is exhaustive given `e`'s type,
-e.g. because it has no constructors. -/
 @[builtinTermElab «nomatch»] def elabNoMatch : TermElab := fun stx expectedType? => do
   match stx with
   | `(nomatch $discrExpr) =>
diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean
index 1fb11f9c36..3adf478b76 100644
--- a/src/Lean/Elab/Quotation.lean
+++ b/src/Lean/Elab/Quotation.lean
@@ -649,23 +649,6 @@ def match_syntax.expand (stx : Syntax) : TermElabM Syntax := do
     return stx
   | _ => throwUnsupportedSyntax
 
-/--
-  Syntactic pattern match. Matches a `Syntax` value against quotations, pattern variables, or `_`.
-
-  Quoted identifiers only match identical identifiers - custom matching such as by the preresolved names only should be done explicitly.
-
-  `Syntax.atom`s are ignored during matching by default except when part of a built-in literal.
-  For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they should participate in matching.
-  For example, in
-  ```lean
-  syntax "c" ("foo" <|> "bar") ...
-  ```
-  `foo` and `bar` are indistinguishable during matching, but in
-  ```lean
-  syntax foo := "foo"
-  syntax "c" (foo <|> "bar") ...
-  ```
-  they are not. -/
 @[builtinTermElab «match»] def elabMatchSyntax : TermElab :=
   adaptExpander match_syntax.expand
 
diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean
index f1cf04a25c..84b5dc800b 100644
--- a/src/Lean/Elab/StructInst.lean
+++ b/src/Lean/Elab/StructInst.lean
@@ -15,7 +15,7 @@ open Std (HashMap)
 open Meta
 open TSyntax.Compat
 
-/--
+/-
   Structure instances are of the form:
 
       "{" >> optional (atomic (sepBy1 termParser ", " >> " with "))
@@ -896,13 +896,6 @@ private def elabStructInstAux (stx : Syntax) (expectedType? : Option Expr) (sour
   synthesizeAppInstMVars instMVars r
   return r
 
-/-- Structure instance. `{ x := e, ... }` assigns `e` to field `x`, which may be
-inherited. If `e` is itself a variable called `x`, it can be elided:
-`fun y => { x := 1, y }`.
-A *structure update* of an existing value can be given via `with`:
-`{ point with x := 1 }`.
-The structure type can be specified if not inferable:
-`{ x := 1, y := 2 : Point }`. -/
 @[builtinTermElab structInst] def elabStructInst : TermElab := fun stx expectedType? => do
   match (← expandNonAtomicExplicitSources stx) with
   | some stxNew => withMacroExpansion stx stxNew <| elabTerm stxNew expectedType?
diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index 6448faf59d..41f0058b74 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -176,11 +176,17 @@ builtin_initialize
 end Command
 
 namespace Term
-/-- `open Foo in e` is like `open Foo` but scoped to a single term. -/
+/--
+`open Foo in e` is like `open Foo` but scoped to a single term.
+It makes the given namespaces available in the term `e`.
+-/
 @[builtinTermParser] def «open» := leading_parser:leadPrec
   "open " >> Command.openDecl >> withOpenDecl (" in " >> termParser)
 
-/-- `set_option opt val in e` is like `set_option opt val` but scoped to a single term. -/
+/--
+`set_option opt val in e` is like `set_option opt val` but scoped to a single term.
+It sets the option `opt` to the value `val` in the term `e`.
+-/
 @[builtinTermParser] def «set_option» := leading_parser:leadPrec
   "set_option " >> ident >> ppSpace >> Command.optionValue >> " in " >> termParser
 end Term
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 38f925b603..18da324c2b 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -53,6 +53,7 @@ namespace Term
 
 /-! # Built-in parsers -/
 
+/-- `by tac` constructs a term of the expected type by running the tactic(s) `tac`. -/
 @[builtinTermParser] def byTactic := leading_parser:leadPrec ppAllowUngrouped >> "by " >> Tactic.tacticSeq
 
 /--
@@ -72,17 +73,41 @@ def optSemicolon (p : Parser) : Parser := ppDedent $ semicolonOrLinebreak >> ppL
 @[builtinTermParser] def scientific : Parser := checkPrec maxPrec >> scientificLit
 @[builtinTermParser] def str : Parser := checkPrec maxPrec >> strLit
 @[builtinTermParser] def char : Parser := checkPrec maxPrec >> charLit
+/-- A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. -/
 @[builtinTermParser] def type := leading_parser "Type" >> optional (checkWsBefore "" >> checkPrec leadPrec >> checkColGt >> levelParser maxPrec)
+/-- A specific universe in Lean's infinite hierarchy of universes. -/
 @[builtinTermParser] def sort := leading_parser "Sort" >> optional (checkWsBefore "" >> checkPrec leadPrec >> checkColGt >> levelParser maxPrec)
+/-- The universe of propositions. `Prop ≡ Sort 0`. -/
 @[builtinTermParser] def prop := leading_parser "Prop"
+/-- A placeholder term, to be synthesized by unification. -/
 @[builtinTermParser] def hole := leading_parser "_"
 @[builtinTermParser] def syntheticHole := leading_parser "?" >> (ident <|> hole)
+/-- A temporary placeholder for a missing proof or value. -/
 @[builtinTermParser] def «sorry» := leading_parser "sorry"
 @[builtinTermParser] def cdot   := leading_parser symbol "·" <|> "."
 def typeAscription := leading_parser " : " >> termParser
 def tupleTail      := leading_parser ", " >> sepBy1 termParser ", "
 def parenSpecial : Parser := optional (tupleTail <|> typeAscription)
+/--
+You can use parentheses for
+- Grouping expressions, e.g., `a * (b + c)`.
+- Creating tuples, e.g., `(a, b, c)` is notation for `Prod.mk a (Prod.mk b c)`.
+- Performing type ascription, e.g., `(0 : Int)` instructs Lean to process `0` as a value of type `Int`.
+- Creating `Unit.unit`, `()` is just a shorthand for `Unit.unit`.
+- Creating simple functions when combined with `·`. Here are some examples:
+  - `(· + 1)` is shorthand for `fun x => x + 1`
+  - `(· + ·)` is shorthand for `fun x y => x + y`
+  - `(f · a b)` is shorthand for `fun x => f x a b`
+  - `(h (· + 1) ·)` is shorthand for `fun x => h (fun y => y + 1) x`
+-/
 @[builtinTermParser] def paren := leading_parser "(" >> (withoutPosition (withoutForbidden (optional (ppDedentIfGrouped termParser >> parenSpecial)))) >> ")"
+/--
+The *anonymous constructor* `⟨e, ...⟩` is equivalent to `c e ...` if the
+expected type is an inductive type with a single constructor `c`.
+If more terms are given than `c` has parameters, the remaining arguments
+are turned into a new anonymous constructor application. For example,
+`⟨a, b, c⟩ : α × (β × γ)` is equivalent to `⟨a, ⟨b, c⟩⟩`.
+-/
 @[builtinTermParser] def anonymousCtor := leading_parser "⟨" >> sepBy termParser ", " >> "⟩"
 def optIdent : Parser := optional (atomic (ident >> " : "))
 def fromTerm   := leading_parser "from " >> termParser
@@ -95,12 +120,25 @@ def structInstLVal   := leading_parser (ident <|> fieldIdx <|> structInstArrayRe
 def structInstField  := ppGroup $ leading_parser structInstLVal >> " := " >> termParser
 def structInstFieldAbbrev := leading_parser atomic (ident >> notFollowedBy ("." <|> ":=" <|> symbol "[") "invalid field abbreviation") -- `x` is an abbreviation for `x := x`
 def optEllipsis      := leading_parser optional ".."
+/--
+Structure instance. `{ x := e, ... }` assigns `e` to field `x`, which may be
+inherited. If `e` is itself a variable called `x`, it can be elided:
+`fun y => { x := 1, y }`.
+A *structure update* of an existing value can be given via `with`:
+`{ point with x := 1 }`.
+The structure type can be specified if not inferable:
+`{ x := 1, y := 2 : Point }`.
+-/
 @[builtinTermParser] def structInst := leading_parser "{" >> ppHardSpace >> optional (atomic (sepBy1 termParser ", " >> " with "))
   >> sepByIndent (structInstFieldAbbrev <|> structInstField) ", " (allowTrailingSep := true)
   >> optEllipsis
   >> optional (" : " >> termParser) >> " }"
 def typeSpec := leading_parser " : " >> termParser
 def optType : Parser := optional typeSpec
+/--
+`@x` disables automatic insertion of implicit parameters of the constant `x`.
+`@e` for any term `e` also disables the insertion of implicit lambdas at this position.
+-/
 @[builtinTermParser] def explicit := leading_parser "@" >> termParser maxPrec
 @[builtinTermParser] def inaccessible := leading_parser ".(" >> termParser >> ")"
 def binderIdent : Parser  := ident <|> hole
@@ -158,7 +196,42 @@ def generalizingParam := leading_parser atomic ("(" >> nonReservedSymbol "genera
 
 def motive := leading_parser atomic ("(" >> nonReservedSymbol "motive" >> " := ") >> termParser >> ")" >> ppSpace
 
+/--
+Pattern matching. `match e, ... with | p, ... => f | ...` matches each given
+term `e` against each pattern `p` of a match alternative. When all patterns
+of an alternative match, the `match` term evaluates to the value of the
+corresponding right-hand side `f` with the pattern variables bound to the
+respective matched values.
+When not constructing a proof, `match` does not automatically substitute variables
+matched on in dependent variables' types. Use `match (generalizing := true) ...` to
+enforce this.
+
+Syntax quotations can also be used in a pattern match.
+This matches a `Syntax` value against quotations, pattern variables, or `_`.
+
+Quoted identifiers only match identical identifiers - custom matching such as by the preresolved
+names only should be done explicitly.
+
+`Syntax.atom`s are ignored during matching by default except when part of a built-in literal.
+For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they
+should participate in matching.
+For example, in
+```lean
+syntax "c" ("foo" <|> "bar") ...
+```
+`foo` and `bar` are indistinguishable during matching, but in
+```lean
+syntax foo := "foo"
+syntax "c" (foo <|> "bar") ...
+```
+they are not.
+-/
 @[builtinTermParser] def «match» := leading_parser:leadPrec "match " >> optional generalizingParam >> optional motive >> sepBy1 matchDiscr ", " >> " with " >> ppDedent matchAlts
+/--
+Empty match/ex falso. `nomatch e` is of arbitrary type `α : Sort u` if
+Lean can show that an empty set of patterns is exhaustive given `e`'s type,
+e.g. because it has no constructors.
+-/
 @[builtinTermParser] def «nomatch» := leading_parser:leadPrec "nomatch " >> termParser
 
 def funImplicitBinder := withAntiquot (mkAntiquot "implicitBinder" ``implicitBinder) <| atomic (lookahead ("{" >> many1 binderIdent >> (symbol " : " <|> "}"))) >> implicitBinder
@@ -174,7 +247,12 @@ def withAnonymousAntiquot := leading_parser atomic ("(" >> nonReservedSymbol "wi
 @[builtinTermParser] def «trailing_parser» := leading_parser:leadPrec "trailing_parser " >> optExprPrecedence >> optExprPrecedence >> termParser
 
 @[builtinTermParser] def borrowed   := leading_parser "@& " >> termParser leadPrec
+/-- A literal of type `Name`. -/
 @[builtinTermParser] def quotedName := leading_parser nameLit
+/--
+A resolved name literal. Evaluates to the full name of the given constant if
+existent in the current context, or else fails.
+-/
 -- use `rawCh` because ``"`" >> ident`` overlaps with `nameLit`, with the latter being preferred by the tokenizer
 -- note that we cannot use ```"``"``` as a new token either because it would break `precheckedQuot`
 @[builtinTermParser] def doubleQuotedName := leading_parser "`" >> checkNoWsBefore >> rawCh '`' (trailingWs := false) >> ident
@@ -272,7 +350,14 @@ def matchAltsWhereDecls := leading_parser matchAlts >> optional whereDecls
 @[builtinTermParser] def forInMacro := leading_parser "for_in% " >> termParser maxPrec >> termParser maxPrec >> termParser maxPrec
 @[builtinTermParser] def forInMacro' := leading_parser "for_in'% " >> termParser maxPrec >> termParser maxPrec >> termParser maxPrec
 
+/-- A macro which evaluates to the name of the currently elaborating declaration. -/
 @[builtinTermParser] def declName           := leading_parser "decl_name%"
+/--
+* `with_decl_name% id e` elaborates `e` in a context while changing the effective
+  declaration name to `id`.
+* `with_decl_name% ?id e` does the same, but resolves `id` as a new definition name
+  (appending the current namespaces).
+-/
 @[builtinTermParser] def withDeclName       := leading_parser "with_decl_name% " >> optional "?" >> ident >> termParser
 @[builtinTermParser] def typeOf             := leading_parser "type_of% " >> termParser maxPrec
 @[builtinTermParser] def ensureTypeOf       := leading_parser "ensure_type_of% " >> termParser maxPrec >> strLit >> termParser
@@ -311,12 +396,21 @@ def isIdent (stx : Syntax) : Bool :=
   -- antiquotations should also be allowed where an identifier is expected
   stx.isAntiquot || stx.isIdent
 
+/-- `x.{u, ...}` explicitly specifies the universes `u, ...` of the constant `x`. -/
 @[builtinTermParser] def explicitUniv : TrailingParser := trailing_parser checkStackTop isIdent "expected preceding identifier" >> checkNoWsBefore "no space before '.{'" >> ".{" >> sepBy1 levelParser ", " >> "}"
+/-- `x@e` matches the pattern `e` and binds its value to the identifier `x`. -/
 @[builtinTermParser] def namedPattern : TrailingParser := trailing_parser checkStackTop isIdent "expected preceding identifier" >> checkNoWsBefore "no space before '@'" >> "@" >> optional (atomic (ident >> ":")) >> termParser maxPrec
 
+/-- `e |>.x` is a shorthand for `(e).x`. It is especially useful for avoiding parentheses with repeated applications. -/
 @[builtinTermParser] def pipeProj   := trailing_parser:minPrec " |>." >> checkNoWsBefore >> (fieldIdx <|> rawIdent) >> many argument
 @[builtinTermParser] def pipeCompletion := trailing_parser:minPrec " |>."
 
+/--
+`h ▸ e` is a macro built on top of `Eq.rec` and `Eq.symm` definitions.
+Given `h : a = b` and `e : p a`, the term `h ▸ e` has type `p b`.
+You can also view `h ▸ e` as a "type casting" operation where you change the type of `e` by using `h`.
+See the Chapter "Quantifiers and Equality" in the manual "Theorem Proving in Lean" for additional information.
+-/
 @[builtinTermParser] def subst := trailing_parser:75 " ▸ " >> sepBy1 (termParser 75) " ▸ "
 
 -- NOTE: Doesn't call `categoryParser` directly in contrast to most other "static" quotations, so call `evalInsideQuot` explicitly
@@ -326,9 +420,23 @@ def bracketedBinderF := bracketedBinder  -- no default arg
 @[builtinTermParser] def matchDiscr.quot : Parser := leading_parser "`(matchDiscr|"  >> incQuotDepth (evalInsideQuot ``matchDiscr matchDiscr) >> ")"
 @[builtinTermParser] def attr.quot : Parser := leading_parser "`(attr|"  >> incQuotDepth attrParser >> ")"
 
+/--
+`panic! msg` formally evaluates to `@Inhabited.default α` if the expected type
+`α` implements `Inhabited`.
+At runtime, `msg` and the file position are printed to stderr unless the C
+function `lean_set_panic_messages(false)` has been executed before. If the C
+function `lean_set_exit_on_panic(true)` has been executed before, the process is
+then aborted.
+-/
 @[builtinTermParser] def panic       := leading_parser:leadPrec "panic! " >> termParser
+/-- A shorthand for `panic! "unreachable code has been reached"`. -/
 @[builtinTermParser] def unreachable := leading_parser:leadPrec "unreachable!"
+/--
+`dbg_trace e; body` evaluates to `body` and prints `e` (which can be an
+interpolated string literal) to stderr. It should only be used for debugging.
+-/
 @[builtinTermParser] def dbgTrace    := leading_parser:leadPrec withPosition ("dbg_trace" >> ((interpolatedStr termParser) <|> termParser)) >> optSemicolon termParser
+/-- `assert! cond` panics if `cond` evaluates to `false`. -/
 @[builtinTermParser] def assert      := leading_parser:leadPrec withPosition ("assert! " >> termParser) >> optSemicolon termParser
 
 
diff --git a/src/Lean/Widget/UserWidget.lean b/src/Lean/Widget/UserWidget.lean
index 707a797de3..c4f454e805 100644
--- a/src/Lean/Widget/UserWidget.lean
+++ b/src/Lean/Widget/UserWidget.lean
@@ -168,11 +168,9 @@ def saveWidgetInfo [Monad m] [MonadEnv m] [MonadError m] [MonadInfoTree m] (widg
   }
   pushInfoLeaf info
 
-/-!  # Widget command
-
-Use `#widget <widgetname> <props>` to display a widget.
--/
+/-!  # Widget command -/
 
+/-- Use `#widget <widgetname> <props>` to display a widget. Useful for debugging widgets. -/
 syntax (name := widgetCmd) "#widget " ident term : command
 
 open Lean Lean.Meta Lean.Elab Lean.Elab.Term in
@@ -184,7 +182,6 @@ private opaque evalJson (stx : Syntax) : TermElabM Json
 
 open Elab Command in
 
-/-- Use this to place a widget. Useful for debugging widgets. -/
 @[commandElab widgetCmd] def elabWidgetCmd : CommandElab := fun
   | stx@`(#widget $id:ident $props) => do
     let props : Json ← runTermElabM fun _ => evalJson props
diff --git a/tests/lean/1021.lean.expected.out b/tests/lean/1021.lean.expected.out
index a0982f896f..ef76cce863 100644
--- a/tests/lean/1021.lean.expected.out
+++ b/tests/lean/1021.lean.expected.out
@@ -1,8 +1,8 @@
-some { range := { pos := { line := 149, column := 41 },
+some { range := { pos := { line := 134, column := 41 },
     charUtf16 := 41,
-    endPos := { line := 155, column := 31 },
+    endPos := { line := 140, column := 31 },
     endCharUtf16 := 31 },
-  selectionRange := { pos := { line := 149, column := 45 },
+  selectionRange := { pos := { line := 134, column := 45 },
     charUtf16 := 45,
-    endPos := { line := 149, column := 57 },
+    endPos := { line := 134, column := 57 },
     endCharUtf16 := 57 } }
diff --git a/tests/lean/interactive/hoverBinderUndescore.lean.expected.out b/tests/lean/interactive/hoverBinderUndescore.lean.expected.out
index 1974084179..5fdb8faa98 100644
--- a/tests/lean/interactive/hoverBinderUndescore.lean.expected.out
+++ b/tests/lean/interactive/hoverBinderUndescore.lean.expected.out
@@ -2,29 +2,47 @@
  "position": {"line": 1, "character": 5}}
 {"range":
  {"start": {"line": 1, "character": 5}, "end": {"line": 1, "character": 6}},
- "contents": {"value": "```lean\nNat\n```", "kind": "markdown"}}
+ "contents":
+ {"value":
+  "```lean\nNat\n```\n***\nA placeholder term, to be synthesized by unification. ",
+  "kind": "markdown"}}
 {"textDocument": {"uri": "file://hoverBinderUndescore.lean"},
  "position": {"line": 1, "character": 7}}
 {"range":
  {"start": {"line": 1, "character": 7}, "end": {"line": 1, "character": 8}},
- "contents": {"value": "```lean\nBool\n```", "kind": "markdown"}}
+ "contents":
+ {"value":
+  "```lean\nBool\n```\n***\nA placeholder term, to be synthesized by unification. ",
+  "kind": "markdown"}}
 {"textDocument": {"uri": "file://hoverBinderUndescore.lean"},
  "position": {"line": 6, "character": 6}}
 {"range":
  {"start": {"line": 6, "character": 6}, "end": {"line": 6, "character": 7}},
- "contents": {"value": "```lean\nNat\n```", "kind": "markdown"}}
+ "contents":
+ {"value":
+  "```lean\nNat\n```\n***\nA placeholder term, to be synthesized by unification. ",
+  "kind": "markdown"}}
 {"textDocument": {"uri": "file://hoverBinderUndescore.lean"},
  "position": {"line": 6, "character": 8}}
 {"range":
  {"start": {"line": 6, "character": 8}, "end": {"line": 6, "character": 9}},
- "contents": {"value": "```lean\nBool\n```", "kind": "markdown"}}
+ "contents":
+ {"value":
+  "```lean\nBool\n```\n***\nA placeholder term, to be synthesized by unification. ",
+  "kind": "markdown"}}
 {"textDocument": {"uri": "file://hoverBinderUndescore.lean"},
  "position": {"line": 11, "character": 6}}
 {"range":
  {"start": {"line": 11, "character": 6}, "end": {"line": 11, "character": 7}},
- "contents": {"value": "```lean\nNat\n```", "kind": "markdown"}}
+ "contents":
+ {"value":
+  "```lean\nNat\n```\n***\nA placeholder term, to be synthesized by unification. ",
+  "kind": "markdown"}}
 {"textDocument": {"uri": "file://hoverBinderUndescore.lean"},
  "position": {"line": 11, "character": 8}}
 {"range":
  {"start": {"line": 11, "character": 8}, "end": {"line": 11, "character": 9}},
- "contents": {"value": "```lean\nBool\n```", "kind": "markdown"}}
+ "contents":
+ {"value":
+  "```lean\nBool\n```\n***\nA placeholder term, to be synthesized by unification. ",
+  "kind": "markdown"}}