diff --git a/Manual/BasicTypes/BitVec.lean b/Manual/BasicTypes/BitVec.lean
index 49e8beb19..8ee881bb6 100644
--- a/Manual/BasicTypes/BitVec.lean
+++ b/Manual/BasicTypes/BitVec.lean
@@ -128,14 +128,14 @@ If the literal is too large to fit in the specified number of bits, then it is t
 $_:num#'$_
 ```
 
-This notation is available only when the `BitVec` namespace has been opened.
+This notation is available only when the {name}`BitVec` namespace has been opened.
 Rather than an explicit width, it expects a proof that the literal value is representable by a bitvector of the corresponding width.
 :::
 
 ::::::leanSection
 :::::example "Bounded Bitvector Literals"
 The bounded bitvector literal notation ensures that literals do not overflow the specified number of bits.
-The notation is only available when the `BitVec` namespace has been opened.
+The notation is only available when the {name}`BitVec` namespace has been opened.
 
 ```lean
 open BitVec
diff --git a/Manual/BasicTypes/Int.lean b/Manual/BasicTypes/Int.lean
index 11c4345f9..468d84895 100644
--- a/Manual/BasicTypes/Int.lean
+++ b/Manual/BasicTypes/Int.lean
@@ -67,7 +67,7 @@ The {inst}`Neg Int` instance allows negation to be used as well.
 open Int
 ```
 
-On top of these instances, there is special syntax for the constructor {lean}`Int.negSucc` that is available when the `Int` namespace is opened.
+On top of these instances, there is special syntax for the constructor {lean}`Int.negSucc` that is available when the {name}`Int` namespace is opened.
 The notation {lean}`-[ n +1]` is suggestive of $`-(n + 1)`, which is the meaning of {lean}`Int.negSucc n`.
 
 :::syntax term (title := "Negative Successor")
diff --git a/Manual/BasicTypes/List/Predicates.lean b/Manual/BasicTypes/List/Predicates.lean
index 025c2e5f3..7c3c54f62 100644
--- a/Manual/BasicTypes/List/Predicates.lean
+++ b/Manual/BasicTypes/List/Predicates.lean
@@ -59,7 +59,7 @@ $_ <+ $_
 
 {includeDocstring List.«term_<+_»}
 
-This syntax is only available when the `List` namespace is opened.
+This syntax is only available when the {name}`List` namespace is opened.
 :::
 
 {docstring List.Perm}
@@ -71,7 +71,7 @@ $_ ~ $_
 
 {includeDocstring List.«term_~_»}
 
-This syntax is only available when the `List` namespace is opened.
+This syntax is only available when the {name}`List` namespace is opened.
 :::
 
 {docstring List.Pairwise}
diff --git a/Manual/BasicTypes/Maps.lean b/Manual/BasicTypes/Maps.lean
index 099a158f9..4f8083312 100644
--- a/Manual/BasicTypes/Maps.lean
+++ b/Manual/BasicTypes/Maps.lean
@@ -181,8 +181,8 @@ A nested inductive type that occurs inside a map or set should be defined in thr
 import Std
 ```
 
-This example requires that `Std.Data.HashMap.RawLemmas` is imported.
-To keep the code shorter, the `Std` namespace is opened:
+This example requires that {name}`Std.Data.HashMap.RawLemmas` is imported.
+To keep the code shorter, the {name}`Std` namespace is opened:
 ```lean
 open Std
 ```
@@ -481,7 +481,7 @@ $_ ~m $_
 
 Unbundled maps separate well-formedness proofs from data.
 This is primarily useful when defining {ref "raw-data"}[nested inductive types].
-To use these variants, import the modules `Std.HashMap.Raw` and `Std.HashMap.RawLemmas`.
+To use these variants, import the modules {name}`Std.HashMap.Raw` and {name}`Std.HashMap.RawLemmas`.
 
 {docstring Std.HashMap.Raw}
 
@@ -605,7 +605,7 @@ $_ ~m $_
 
 Unbundled maps separate well-formedness proofs from data.
 This is primarily useful when defining {ref "raw-data"}[nested inductive types].
-To use these variants, import the modules `Std.DHashMap.Raw` and `Std.DHashMap.RawLemmas`.
+To use these variants, import the modules {name}`Std.DHashMap.Raw` and {name}`Std.DHashMap.RawLemmas`.
 
 {docstring Std.DHashMap.Raw}
 
@@ -852,7 +852,7 @@ $_ ~m $_
 
 Unbundled maps separate well-formedness proofs from data.
 This is primarily useful when defining {ref "raw-data"}[nested inductive types].
-To use these variants, import the modules `Std.HashSet.Raw` and `Std.HashSet.RawLemmas`.
+To use these variants, import the modules {name}`Std.HashSet.Raw` and {name}`Std.HashSet.RawLemmas`.
 
 {docstring Std.HashSet.Raw}
 
@@ -1014,7 +1014,7 @@ The declarations in this section should be imported using `import Std.DTreeMap`.
 
 Unbundled maps separate well-formedness proofs from data.
 This is primarily useful when defining {ref "raw-data"}[nested inductive types].
-To use these variants, import the module `Std.DTreeMap.Raw`.
+To use these variants, import the module {name}`Std.DTreeMap.Raw`.
 
 {docstring Std.DTreeMap.Raw}
 
diff --git a/Manual/BasicTypes/Maps/TreeMap.lean b/Manual/BasicTypes/Maps/TreeMap.lean
index 2cb7ce19e..823c940d2 100644
--- a/Manual/BasicTypes/Maps/TreeMap.lean
+++ b/Manual/BasicTypes/Maps/TreeMap.lean
@@ -261,7 +261,7 @@ The declarations in this section should be imported using `import Std.TreeMap`.
 
 Unbundled maps separate well-formedness proofs from data.
 This is primarily useful when defining {ref "raw-data"}[nested inductive types].
-To use these variants, import the module `Std.TreeMap.Raw`.
+To use these variants, import the module {name}`Std.TreeMap.Raw`.
 
 {docstring Std.TreeMap.Raw}
 
diff --git a/Manual/BasicTypes/Maps/TreeSet.lean b/Manual/BasicTypes/Maps/TreeSet.lean
index 077fca594..9e6a5c657 100644
--- a/Manual/BasicTypes/Maps/TreeSet.lean
+++ b/Manual/BasicTypes/Maps/TreeSet.lean
@@ -160,7 +160,7 @@ tag := "TreeSet"
 
 Unbundled sets separate well-formedness proofs from data.
 This is primarily useful when defining {ref "raw-data"}[nested inductive types].
-To use these variants, import the module `Std.TreeSet.Raw`.
+To use these variants, import the module {name}`Std.TreeSet.Raw`.
 
 {docstring Std.TreeSet.Raw}
 
diff --git a/Manual/BasicTypes/Nat.lean b/Manual/BasicTypes/Nat.lean
index 218079df5..d8fb74ecc 100644
--- a/Manual/BasicTypes/Nat.lean
+++ b/Manual/BasicTypes/Nat.lean
@@ -42,7 +42,7 @@ A proof by induction requires a base case and an induction step.
 The base case is a proof that the statement is true for `0`.
 The induction step is a proof that the truth of the statement for some arbitrary number {lean}`i` implies its truth for {lean}`i + 1`.
 
-This proof uses the lemma `Nat.succ_lt_succ` in its induction step.
+This proof uses the lemma {name}`Nat.succ_lt_succ` in its induction step.
 ```lean
 example (n : Nat) : n < n + 1 := by
   induction n with
@@ -98,19 +98,19 @@ theorem succ_not_zero : ¬n + 1 = 0 :=
 tag := "nat-runtime"
 %%%
 
-The representation suggested by the declaration of `Nat` would be horrendously inefficient, as it's essentially a linked list.
+The representation suggested by the declaration of {name}`Nat` would be horrendously inefficient, as it's essentially a linked list.
 The length of the list would be the number.
 With this representation, addition would take time linear in the size of one of the addends, and numbers would take at least as many machine words as their magnitude in memory.
 Thus, natural numbers have special support in both the kernel and the compiler that avoids this overhead.
 
-In the kernel, there are special `Nat` literal values that use a widely-trusted, efficient arbitrary-precision integer library (usually [GMP](https://gmplib.org/)).
+In the kernel, there are special {name}`Nat` literal values that use a widely-trusted, efficient arbitrary-precision integer library (usually [GMP](https://gmplib.org/)).
 Basic functions such as addition are overridden by primitives that use this representation.
 Because they are part of the kernel, if these primitives did not correspond to their definitions as Lean functions, it could undermine soundness.
 
 In compiled code, sufficiently-small natural numbers are represented without pointer indirections: the lowest-order bit in an object pointer is used to indicate that the value is not, in fact, a pointer, and the remaining bits are used to store the number.
 31 bits are available on 32-bits architectures for pointer-free {lean}`Nat`s, while 63 bits are available on 64-bit architectures.
 In other words, natural numbers smaller than $`2^{31} = 2,147,483,648` or $`2^{63} = 9,223,372,036,854,775,808` do not require allocations.
-If an natural number is too large for this representation, it is instead allocated as an ordinary Lean object that consists of an object header and an arbitrary-precision integer value.
+If a natural number is too large for this representation, it is instead allocated as an ordinary Lean object that consists of an object header and an arbitrary-precision integer value.
 
 ## Performance Notes
 %%%
diff --git a/Manual/BasicTypes/String.lean b/Manual/BasicTypes/String.lean
index 1e8475648..1586b8eda 100644
--- a/Manual/BasicTypes/String.lean
+++ b/Manual/BasicTypes/String.lean
@@ -352,7 +352,7 @@ tag := "string-api-compare"
 %%%
 
 The {inst}`LT String` instance is defined by the lexicographic ordering on strings based on the {inst}`LT Char` instance.
-Logically, this is modeled by the lexicographic ordering on the lists that model strings, so `List.Lex` defines the order.
+Logically, this is modeled by the lexicographic ordering on the lists that model strings, so {name}`List.Lex` defines the order.
 It is decidable, and the decision procedure is overridden at runtime with efficient code that takes advantage of the run-time representation of strings.
 
 {docstring String.le}
diff --git a/Manual/BasicTypes/Sum.lean b/Manual/BasicTypes/Sum.lean
index 4f95dfb61..24bcdbe25 100644
--- a/Manual/BasicTypes/Sum.lean
+++ b/Manual/BasicTypes/Sum.lean
@@ -38,7 +38,7 @@ There are two varieties of the sum type:
 Manually-written Lean code almost always uses only {lean}`Sum`, while {lean}`PSum` is used as part of the implementation of proof automation.
 This is because it imposes problematic constraints that universe level unification cannot solve.
 In particular, this type is in the universe {lean}`Sort (max 1 u v)`, which can cause problems for universe level unification because the equation `max 1 u v = ?u + 1` has no solution in level arithmetic.
-`PSum` is usually only used in automation that constructs sums of arbitrary types.
+{name}`PSum` is usually only used in automation that constructs sums of arbitrary types.
 :::
 ::::
 
diff --git a/Manual/Classes.lean b/Manual/Classes.lean
index 805b9397d..e9296ad12 100644
--- a/Manual/Classes.lean
+++ b/Manual/Classes.lean
@@ -279,7 +279,7 @@ def Heap.insert [Ord α] (x : α) (xs : Heap α) : Heap α :=
 
 The problem is that a heap constructed with one {name}`Ord` instance may later be used with another, leading to the breaking of the heap invariant.
 
-One way to correct this is to make the heap type depend on the selected `Ord` instance:
+One way to correct this is to make the heap type depend on the selected {name}`Ord` instance:
 ```lean
 structure Heap' (α : Type u) [Ord α] where
   contents : Array α
diff --git a/Manual/Classes/BasicClasses.lean b/Manual/Classes/BasicClasses.lean
index 4c44f0f24..eade490f7 100644
--- a/Manual/Classes/BasicClasses.lean
+++ b/Manual/Classes/BasicClasses.lean
@@ -53,7 +53,7 @@ There are two primary ways to order the values of a type:
 
 {docstring Ord}
 
-The {name}`compare` method is exported, so no explicit `Ord` namespace is required to use it.
+The {name}`compare` method is exported, so no explicit {name}`Ord` namespace is required to use it.
 
 {docstring compareOn}
 
@@ -193,8 +193,8 @@ true
 
 # Minimum and Maximum Values
 
-The classes `Max` and `Min` provide overloaded operators for choosing the greater or lesser of two values.
-These should be in agreement with `Ord`, `LT`, and `LE` instances, if they exist, but there is no mechanism to enforce this.
+The classes {name}`Max` and {name}`Min` provide overloaded operators for choosing the greater or lesser of two values.
+These should be in agreement with {name}`Ord`, {name}`LT`, and {name}`LE` instances, if they exist, but there is no mechanism to enforce this.
 
 {docstring Min}
 
@@ -222,7 +222,7 @@ tag := "decidable-propositions"
 
 A proposition is {deftech}_decidable_ if it can be checked algorithmically.{index}[decidable]{index (subterm := "decidable")}[proposition]
 The Law of the Excluded Middle means that every proposition is true or false, but it provides no way to check which of the two cases holds, which can often be useful.
-By default, only algorithmic {lean}`Decidable` instances for which code can be generated are in scope; opening the `Classical` namespace makes every proposition decidable.
+By default, only algorithmic {lean}`Decidable` instances for which code can be generated are in scope; opening the {name}`Classical` namespace makes every proposition decidable.
 
 {docstring Decidable}
 
@@ -253,7 +253,7 @@ failed to synthesize instance of type class
 Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
 ```
 
-Opening `Classical` makes every proposition decidable; however, declarations and examples that use this fact must be marked {keywordOf Lean.Parser.Command.declaration}`noncomputable` to indicate that code should not be generated for them.
+Opening {name}`Classical` makes every proposition decidable; however, declarations and examples that use this fact must be marked {keywordOf Lean.Parser.Command.declaration}`noncomputable` to indicate that code should not be generated for them.
 ```lean
 open Classical
 noncomputable example (f g : Nat → Nat) : Decidable (f = g) :=
diff --git a/Manual/Classes/DerivingHandlers.lean b/Manual/Classes/DerivingHandlers.lean
index cdccbf7ea..766a0f4c3 100644
--- a/Manual/Classes/DerivingHandlers.lean
+++ b/Manual/Classes/DerivingHandlers.lean
@@ -114,7 +114,7 @@ class IsEnum (α : Type) where
 ```
 
 For inductive types that are trivial enumerations, where no constructor expects any parameters, instances of this class are quite repetitive.
-The instance for `Bool` is typical:
+The instance for {name}`Bool` is typical:
 ```lean
 instance : IsEnum Bool where
   size := 2
diff --git a/Manual/Classes/InstanceSynth.lean b/Manual/Classes/InstanceSynth.lean
index 5ec71e8bd..b28987802 100644
--- a/Manual/Classes/InstanceSynth.lean
+++ b/Manual/Classes/InstanceSynth.lean
@@ -178,7 +178,7 @@ Once the search for {lean}`Nonempty Nat` succeeds, the {keywordOf Lean.Parser.Co
 # Candidate Instances
 
 Instance synthesis uses both local and global instances in its search.
-{deftech}_Local instances_ are those available in the local context; they may be either parameters to a function or locally defined with `let`. {TODO}[xref to docs for `let`]
+{deftech}_Local instances_ are those available in the local context; they may be either parameters to a function or locally defined with {keywordOf Lean.Parser.Term.let}`let`. {TODO}[xref to docs for `let`]
 Local instances do not need to be indicated specially; any local variable whose type is a type class is a candidate for instance synthesis.
 {deftech}_Global instances_ are those available in the global environment; every global instance is a defined name with the {attr}`instance` attribute applied.{margin}[{keywordOf Lean.Parser.Command.declaration}`instance` declarations automatically apply the {attr}`instance` attribute.]
 
diff --git a/Manual/ErrorExplanations/DependsOnNoncomputable.lean b/Manual/ErrorExplanations/DependsOnNoncomputable.lean
index 2246e6b4d..bcf04fa4e 100644
--- a/Manual/ErrorExplanations/DependsOnNoncomputable.lean
+++ b/Manual/ErrorExplanations/DependsOnNoncomputable.lean
@@ -81,8 +81,8 @@ def endsOrDefault (ns : List Nat) : Nat × Nat :=
 ```
 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
+version of `getOrDefault` (using the {name}`Inhabited` type class), allowing `endsOrDefault` to be
+computable. (The differences between {name}`Inhabited` and {name}`Nonempty` are described in the documentation
 of inhabited types in the manual section on {ref "basic-classes"}[Basic Classes].)
 :::
 
@@ -114,9 +114,9 @@ noncomputable def fromImage (f : Nat → Nat) (y : Nat) :=
   else
     f 0
 ```
-The `Classical` namespace contains `Decidable` instances that are not computable. These are a common
+The {name}`Classical` namespace contains {name}`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`.
+definition. In the above example, for instance, a {name}`Decidable` instance for the proposition
+{lean}`∃ x, f x = y` is synthesized using a {name}`Classical` decidability instance; therefore, {name}`fromImage` must
+be marked {keyword}`noncomputable`.
 :::
diff --git a/Manual/ErrorExplanations/InductionWithNoAlts.lean b/Manual/ErrorExplanations/InductionWithNoAlts.lean
index 4912fd609..d7124facc 100644
--- a/Manual/ErrorExplanations/InductionWithNoAlts.lean
+++ b/Manual/ErrorExplanations/InductionWithNoAlts.lean
@@ -18,8 +18,8 @@ shortTitle := "inductionWithNoAlts"
 {errorExplanationHeader lean.inductionWithNoAlts}
 
 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.
+individual cases of the proof. However, the {tactic}`induction'` tactic in Mathlib and the specialized
+{tactic}`induction` tactic for natural numbers used in the Natural Number Game follows a different pattern.
 
 # Examples
 
@@ -46,7 +46,7 @@ theorem zero_mul (m : Nat) : 0 * m = 0 := by
     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
+proof will work if you {keywordOf Lean.Parser.Command.import}`import` Mathlib and replace {tactic}`induction` with {tactic}`induction'`. Induction tactics
 in basic Lean expect the {keyword}`with` keyword to be followed by a series of cases, and the names
 for the inductive case are provided in the {name Nat.succ}`succ` case rather than being provided
 up-front.
diff --git a/Manual/ErrorExplanations/InductiveParamMissing.lean b/Manual/ErrorExplanations/InductiveParamMissing.lean
index b6da0198a..95b6bc797 100644
--- a/Manual/ErrorExplanations/InductiveParamMissing.lean
+++ b/Manual/ErrorExplanations/InductiveParamMissing.lean
@@ -67,8 +67,8 @@ inductive RoseTree.All (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
+Because the {name}`RoseTree.All` type constructor must be partially applied in the argument to {name}`List.All`,
+the unspecified argument (`t`) must not be a parameter of the {name}`RoseTree.All` predicate. Making it an
+index to the right of the colon in the header of {name}`RoseTree.All` allows this partial application to
 succeed.
 :::
diff --git a/Manual/ErrorExplanations/InferBinderTypeFailed.lean b/Manual/ErrorExplanations/InferBinderTypeFailed.lean
index 69ff936cd..6f3c82b20 100644
--- a/Manual/ErrorExplanations/InferBinderTypeFailed.lean
+++ b/Manual/ErrorExplanations/InferBinderTypeFailed.lean
@@ -101,10 +101,10 @@ Note: Because this declaration's type has been explicitly provided, all paramete
 example : True :=
   trivial
 ```
-This code is invalid because it attempts to give a name to an `example` declaration. Examples cannot
+This code is invalid because it attempts to give a name to an {keywordOf Lean.Parser.Command.example}`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`.
+defined using a declaration form that supports naming, such as {keywordOf Lean.Parser.Command.declaration}`def` or {keywordOf Lean.Parser.Command.declaration}`theorem`.
 :::
 
 :::errorExample "Attempting to Define Multiple Opaque Constants at Once"
@@ -120,9 +120,9 @@ Note: Multiple constants cannot be declared in a single declaration. The identif
 opaque m : Nat
 opaque n : Nat
 ```
-This example incorrectly attempts to define multiple constants with a single `opaque` declaration.
+This example incorrectly attempts to define multiple constants with a single {keywordOf Lean.Parser.Command.declaration}`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
+after {keywordOf Lean.Parser.Command.declaration}`opaque` or {keywordOf Lean.Parser.Command.declaration}`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.
diff --git a/Manual/ErrorExplanations/InferDefTypeFailed.lean b/Manual/ErrorExplanations/InferDefTypeFailed.lean
index 842fe0b99..85d3f7766 100644
--- a/Manual/ErrorExplanations/InferDefTypeFailed.lean
+++ b/Manual/ErrorExplanations/InferDefTypeFailed.lean
@@ -34,7 +34,7 @@ Note that when an explicit resulting type is provided—even if that type contai
 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
+type in a {keywordOf Lean.Parser.Command.declaration}`theorem` declaration: the {keywordOf Lean.Parser.Command.declaration}`theorem` syntax requires a type annotation, and the elaborator
 will never attempt to use the theorem body to infer the proposition being proved.
 
 # Examples
@@ -56,7 +56,7 @@ def emptyNats :=
   List.nil (α := Nat)
 ```
 
-Here, Lean is unable to infer the value of the parameter `α` of the `List` type constructor, which
+Here, Lean is unable to infer the value of the parameter `α` of the {name}`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
diff --git a/Manual/ErrorExplanations/UnknownIdentifier.lean b/Manual/ErrorExplanations/UnknownIdentifier.lean
index 157d597e5..b8fda24f1 100644
--- a/Manual/ErrorExplanations/UnknownIdentifier.lean
+++ b/Manual/ErrorExplanations/UnknownIdentifier.lean
@@ -98,14 +98,14 @@ 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
+In this example, the identifier `rgb` on the last line does not resolve to the {name}`Color` constructor
+of that name. This is because the constructor's name is actually {name}`Color.rgb`: all constructors of an
+inductive type have names in that type's namespace. Because the {name}`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
+One way to resolve this error is to provide the fully qualified constructor name {lean}`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
+{name}`Color`. Alternatively, one can open the {name}`Color` namespace and continue to omit the {name}`Color` prefix
 from the identifier.
 :::
 
diff --git a/Manual/Grind/Algebra.lean b/Manual/Grind/Algebra.lean
index 63fc6714e..325a2a51e 100644
--- a/Manual/Grind/Algebra.lean
+++ b/Manual/Grind/Algebra.lean
@@ -26,13 +26,13 @@ set_option maxHeartbeats 300000
 tag := "grind-ring"
 %%%
 
-The `ring` solver in {tactic}`grind` is inspired by Gröbner basis computation procedures and term rewriting completion.
+The {name}`ring` solver in {tactic}`grind` is inspired by Gröbner basis computation procedures and term rewriting completion.
 It views multivariate polynomials as rewriting rules.
 For example, the polynomial equality `x * y + x - 2 = 0` is treated as a rewriting rule `x * y ↦ -x + 2`.
 It uses superposition to ensure the rewriting system is confluent.
 
-The following examples demonstrate goals that can be decided by the `ring` solver.
-In these examples, the `Lean` and `Lean.Grind` namespaces are open:
+The following examples demonstrate goals that can be decided by the {name}`ring` solver.
+In these examples, the {name}`Lean` and {name}`Lean.Grind` namespaces are open:
 ```lean
 open Lean Grind
 ```
@@ -127,7 +127,7 @@ tag := "grind-ring-classes"
 %%%
 
 :::paragraph
-Users can enable the `ring` solver for their own types by providing instances of the following {tech (key := "type class")}[type classes], all in the `Lean.Grind` namespace:
+Users can enable the {name}`ring` solver for their own types by providing instances of the following {tech (key := "type class")}[type classes], all in the {name}`Lean.Grind` namespace:
 
 * {name Lean.Grind.Semiring}`Semiring`
 
@@ -151,8 +151,8 @@ The capabilities of the algebraic solvers will, of course, degrade when some are
 :::
 
 The Lean standard library contains the applicable instances for the types defined in the standard library.
-By providing these instances, other libraries can also enable {tactic}`grind`'s `ring` solver.
-For example, the Mathlib `CommRing` type class implements `Lean.Grind.CommRing` to ensure the `ring` solver works out-of-the-box.
+By providing these instances, other libraries can also enable {tactic}`grind`'s {name}`ring` solver.
+For example, the Mathlib {name}`CommRing` type class implements {name}`Lean.Grind.CommRing` to ensure the {name}`ring` solver works out-of-the-box.
 
 ## Algebraic Structures
 
@@ -214,7 +214,7 @@ tag := "NoNatZeroDivisors"
 %%%
 
 
-The class `NoNatZeroDivisors` is used to control coefficient growth.
+The class {name}`NoNatZeroDivisors` is used to control coefficient growth.
 For example, the polynomial `2 * x * y + 4 * z = 0` is simplified to `x * y + 2 * z = 0`.
 It also used when processing disequalities.
 
@@ -316,9 +316,9 @@ h_2 : ¬y * x = 1
 tag := "AddRightCancel"
 %%%
 
-The `ring` solver automatically embeds `CommSemiring`s into a `CommRing` envelope (using the construction `Lean.Grind.Ring.OfSemiring.Q`).
-However, the embedding is injective only when the `CommSemiring` implements the type class `AddRightCancel`.
-`Nat` is an example of  a commutative semiring that implements `AddRightCancel`.
+The {name}`ring` solver automatically embeds {name}`CommSemiring`s into a {name}`CommRing` envelope (using the construction {name}`Lean.Grind.Ring.OfSemiring.Q`).
+However, the embedding is injective only when the {name}`CommSemiring` implements the type class {name}`AddRightCancel`.
+{name}`Nat` is an example of a commutative semiring that implements {name}`AddRightCancel`.
 
 ```lean
 example (x y : Nat) :
diff --git a/Manual/Grind/ExtendedExamples/IfElseNorm.lean b/Manual/Grind/ExtendedExamples/IfElseNorm.lean
index 910505770..33111fa85 100644
--- a/Manual/Grind/ExtendedExamples/IfElseNorm.lean
+++ b/Manual/Grind/ExtendedExamples/IfElseNorm.lean
@@ -202,7 +202,7 @@ and then, whenever performing a branch on a variable, adding a new assignment in
 It also needs to flatten nested if-then-else expressions which have another if-then-else in the “condition” position.
 (This is extracted from Chris Hughes's solution, but without the subtyping.)
 
-Let's work inside the `IfExpr` namespace.
+Let's work inside the {name}`IfExpr` namespace.
 ```lean
 namespace IfExpr
 ```
diff --git a/Manual/Grind/Linarith.lean b/Manual/Grind/Linarith.lean
index 700c93ad5..a028a40d7 100644
--- a/Manual/Grind/Linarith.lean
+++ b/Manual/Grind/Linarith.lean
@@ -27,13 +27,13 @@ open Lean.Grind
 tag := "grind-linarith"
 %%%
 
-The {tactic}`grind` tactic includes a linear arithmetic solver for arbitrary types, called `linarith`, that is used for types not supported by {ref "cutsat"}`cutsat`.
+The {tactic}`grind` tactic includes a linear arithmetic solver for arbitrary types, called {name}`linarith`, that is used for types not supported by {ref "cutsat"}`cutsat`.
 Like the {ref "grind-ring"}`ring` solver, it can be used with any type that has instances of certain type classes.
 It self-configures depending on the availability of these type classes, so it is not necessary to provide all of them to use the solver; however, its capabilities are increased by the availability of more instances.
 This solver is useful for reasoning about the real numbers, ordered vector spaces, and other types that can't be embedded into {name}`Int`.
 
 
-The core functionality of `linarith` is a model-based solver for linear inequalities with integer coefficients.
+The core functionality of {name}`linarith` is a model-based solver for linear inequalities with integer coefficients.
 It can be disabled using the option `grind -linarith`.
 
 
@@ -107,8 +107,8 @@ example (a b c d e f : R) :
 
 :::TODO
 Planned future features
-* Support for `NatModule` (by embedding in the Grothendieck envelope, as we already do for semirings),
-* Better communication between the `ring` and `linarith` solvers.
+* Support for {name}`NatModule` (by embedding in the Grothendieck envelope, as we already do for semirings),
+* Better communication between the {name}`ring` and {name}`linarith` solvers.
   There is currently very little communication between these two solvers.
 * Non-linear arithmetic over ordered rings.
 :::
diff --git a/Manual/Iterators.lean b/Manual/Iterators.lean
index 4fa01a999..fdf599bd3 100644
--- a/Manual/Iterators.lean
+++ b/Manual/Iterators.lean
@@ -384,7 +384,7 @@ Zip Nats Id (ListIterator String) String : Type
 ```leanOutput natfin
 Zip.instFinite₂
 ```
-In contrast, `Nats.iter` has no `Finite` instance because it yields infinitely many values:
+In contrast, {name}`Nats.iter` has no {name}`Finite` instance because it yields infinitely many values:
 ```lean (name := natinf) +error
 #synth Finite Nats Id
 ```
@@ -526,8 +526,8 @@ With the {name}`IteratorCollect` instance in place, {name}`Iter.toArray` now wor
 #['a', 'b', 'c']
 ```
 
-In general, `Iter.toArray` might run forever. One can prove that `abc` is finite, and the above example will terminate after finitely many steps, by
-constructing a `Finite (Triple Char) Id` instance.
+In general, {name}`Iter.toArray` might run forever. One can prove that `abc` is finite, and the above example will terminate after finitely many steps, by
+constructing a {lean}`Finite (Triple Char) Id` instance.
 It's easiest to start at {name}`TriplePos.done` and work backwards toward {name}`TriplePos.fst`, showing that each position in turn has a finite chain of successors:
 
 ```lean
diff --git a/Manual/Language/Functions.lean b/Manual/Language/Functions.lean
index b19d57a0f..8a1e68eb7 100644
--- a/Manual/Language/Functions.lean
+++ b/Manual/Language/Functions.lean
@@ -217,7 +217,7 @@ example : thirdChar #['-', 'x'] = 'A' := rfl
 tag := "function-api"
 %%%
 
-The `Function` namespace contains general-purpose helpers for working with functions.
+The {name}`Function` namespace contains general-purpose helpers for working with functions.
 
 {docstring Function.comp}
 
diff --git a/Manual/Language/InductiveTypes.lean b/Manual/Language/InductiveTypes.lean
index 2a39b9c12..834bdc478 100644
--- a/Manual/Language/InductiveTypes.lean
+++ b/Manual/Language/InductiveTypes.lean
@@ -393,7 +393,7 @@ tag := "inductive-types-runtime-relevance"
 
 
 Types and proofs have no run-time representation.
-That is, if an inductive type is a `Prop`, then its values are erased prior to compilation.
+That is, if an inductive type is a {name}`Prop`, then its values are erased prior to compilation.
 Similarly, all theorem statements and types are erased.
 Types with run-time representations are called {deftech}_relevant_, while types without run-time representations are called {deftech}_irrelevant_.
 
diff --git a/Manual/Language/InductiveTypes/LogicalModel.lean b/Manual/Language/InductiveTypes/LogicalModel.lean
index a7ffa9f52..5c2cb2cb2 100644
--- a/Manual/Language/InductiveTypes/LogicalModel.lean
+++ b/Manual/Language/InductiveTypes/LogicalModel.lean
@@ -28,7 +28,7 @@ tag := "recursors"
 
 Every inductive type is equipped with a {tech}[recursor].
 The recursor is completely determined by the signatures of the type constructor and the constructors.
-Recursors have function types, but they are primitive and are not definable using `fun`.
+Recursors have function types, but they are primitive and are not definable using {keywordOf Lean.Parser.Term.fun}`fun`.
 
 ## Recursor Types
 %%%
diff --git a/Manual/Language/Namespaces.lean b/Manual/Language/Namespaces.lean
index 1831c8e0f..863d77142 100644
--- a/Manual/Language/Namespaces.lean
+++ b/Manual/Language/Namespaces.lean
@@ -28,7 +28,7 @@ Namespaces are orthogonal to {tech}[modules]: a module is a unit of code that is
 A module may contain names in any namespace, and the nesting structure of hierarchical modules is unrelated to that of hierarchical namespaces.
 
 There is a root namespace, ordinarily denoted by simply omitting a namespace.
-It can be explicitly indicated by beginning a name with `_root_`.
+It can be explicitly indicated by beginning a name with {name}`_root_`.
 This can be necessary in contexts where a name would otherwise be interpreted relative to an ambient namespace (e.g. from a {tech}[section scope]) or local scope.
 
 :::example "Explicit Root Namespace"
@@ -48,7 +48,7 @@ end Forest
 "Lemons are green"
 ```
 
-Within the `Forest` namespace, references to {name _root_.color}`color` in the root namespace must be qualified with `_root_`:
+Within the {name}`Forest` namespace, references to {name _root_.color}`color` in the root namespace must be qualified with {name}`_root_`:
 ```lean
 namespace Forest
 def nextStatement :=
@@ -104,7 +104,7 @@ end
 HotDrink.tea : HotDrink
 ```
 
-If a function is defined directly inside the `HotDrink` namespace, then the body of the function is elaborated with the current namespace set to `HotDrink`.
+If a function is defined directly inside the {name}`HotDrink` namespace, then the body of the function is elaborated with the current namespace set to {name}`HotDrink`.
 The constructors are in scope:
 ```lean
 def HotDrink.ofString? : String → Option HotDrink
@@ -120,8 +120,8 @@ inductive ColdDrink where
   | juice
 ```
 
-From within the `HotDrink` namespace, {name}`HotDrink.toString` can be defined without an explicit prefix.
-Defining a function in the `ColdDrink` namespace requires an explicit `_root_` qualifier to avoid defining `HotDrink.ColdDrink.toString`:
+From within the {name}`HotDrink` namespace, {name}`HotDrink.toString` can be defined without an explicit prefix.
+Defining a function in the {name}`ColdDrink` namespace requires an explicit {name}`_root_` qualifier to avoid defining {name}`HotDrink.ColdDrink.toString`:
 ```lean
 namespace HotDrink
 
diff --git a/Manual/Monads/Syntax.lean b/Manual/Monads/Syntax.lean
index 657fd910d..e8ac152c3 100644
--- a/Manual/Monads/Syntax.lean
+++ b/Manual/Monads/Syntax.lean
@@ -623,7 +623,7 @@ def satisfyingIndices (p : α → Prop) [DecidablePred p] (xs : Array α) : Arra
 :::::keepEnv
 ::::leanSection
 
-Iteration with `for`-loops is translated into uses of `ForIn.forIn`, which is an analogue of `ForM.forM` with added support for local mutations and early termination.
+Iteration with {keywordOf Lean.Parser.Term.doFor}`for`-loops is translated into uses of {name}`ForIn.forIn`, which is an analogue of {name}`ForM.forM` with added support for local mutations and early termination.
 {name}`ForIn.forIn` receives an initial value for the local mutable state and a monadic action as parameters, along with the collection being iterated over.
 The monadic action passed to {name}`ForIn.forIn` takes a current state as a parameter and, after carrying out actions in the monad {lean}`m`, returns either {name}`ForInStep.yield` to indicate that iteration should continue with an updated set of local mutable values, or {name}`ForInStep.done` to indicate that {keywordOf Lean.Parser.Term.doBreak}`break` or {keywordOf Lean.Parser.Term.doReturn}`return` was executed.
 When iteration is complete, {name}`ForIn.forIn` returns the final values of the local mutable values.
diff --git a/Manual/Namespaces.lean b/Manual/Namespaces.lean
index 053499324..acd6903d8 100644
--- a/Manual/Namespaces.lean
+++ b/Manual/Namespaces.lean
@@ -113,7 +113,7 @@ If it includes {keyword}`meta`, then the section's declarations are all placed i
 
 :::example "Named Section"
 
-The name {name Greetings.english}`english` is defined in the `Greetings` namespace.
+The name {name Greetings.english}`english` is defined in the {name}`Greetings` namespace.
 
 ```lean
 def Greetings.english := "Hello"
@@ -188,7 +188,7 @@ To close a namespace, the {keywordOf Lean.Parser.Command.end}`end` command requi
 All section scopes introduced by the {keywordOf Lean.Parser.Command.namespace}`namespace` command that introduced part of that suffix are closed.
 
 :::syntax command (title := "Namespace Declarations")
-The `namespace` command modifies the current namespace by appending the provided identifier.
+The {keywordOf Lean.Parser.Command.namespace}`namespace` command modifies the current namespace by appending the provided identifier.
 
 creates a section scope that lasts either until an {keywordOf Lean.Parser.Command.end}`end` command or the end of the file.
 ```grammar
@@ -250,7 +250,7 @@ Rather than opening a section for a single command, the {keywordOf Lean.Parser.C
 The {keywordOf Lean.Parser.Command.in}`in` combinator is right-associative, allowing multiple scope modifications to be stacked.
 
 :::syntax command (title := "Local Section Scopes")
-The `in` command combinator introduces a section scope for a single command.
+The {keywordOf Lean.Parser.Command.in}`in` command combinator introduces a section scope for a single command.
 ```grammar
 $c:command in
 $c:command
@@ -301,7 +301,7 @@ variable $b:bracketedBinder $b:bracketedBinder*
 ```
 :::
 
-The bracketed binders allowed after `variable` match the {ref "bracketed-parameter-syntax"}[syntax used in definition headers].
+The bracketed binders allowed after {keywordOf Lean.Parser.Command.variable}`variable` match the {ref "bracketed-parameter-syntax"}[syntax used in definition headers].
 
 ::::example "Section Variables"
 In this section, automatic implicit parameters are disabled, but a number of section variables are defined.
diff --git a/Manual/NotationsMacros/Delab.lean b/Manual/NotationsMacros/Delab.lean
index 97780996c..d85963c49 100644
--- a/Manual/NotationsMacros/Delab.lean
+++ b/Manual/NotationsMacros/Delab.lean
@@ -282,7 +282,7 @@ open Lean.PrettyPrinter.Delaborator.SubExpr
 :::paragraph
 The monad {name}`DelabM` is a {tech}[reader monad] that includes access to the current position in the {lean}`Expr`.
 Recursive delaboration is performed by adjusting the reader monad's tracked position, rather than by explicitly passing a subexpression to another function.
-The most important functions for working with subexpressions in delaborators are in the namespace `Lean.PrettyPrinter.Delaborator.SubExp`:
+The most important functions for working with subexpressions in delaborators are in the namespace {name}`Lean.PrettyPrinter.Delaborator.SubExpr`:
  * {name}`getExpr` retrieves the current expression for analysis.
  * {name}`withAppFn` adjusts the current position to be that of the function in an application.
  * {name}`withAppArg` adjusts the current position to be that of the argument in an application
diff --git a/Manual/RecursiveDefs/PartialFixpoint/Theory.lean b/Manual/RecursiveDefs/PartialFixpoint/Theory.lean
index 4830a8183..260ba5c2f 100644
--- a/Manual/RecursiveDefs/PartialFixpoint/Theory.lean
+++ b/Manual/RecursiveDefs/PartialFixpoint/Theory.lean
@@ -26,9 +26,9 @@ tag := "partial-fixpoint-theory"
 
 The construction builds on a variant of the Knaster–Tarski theorem: In a chain-complete partial order, every monotone function has a least fixed point.
 
-The necessary theory is found in the `Lean.Order` namespace.
+The necessary theory is found in the {name}`Lean.Order` namespace.
 This is not meant to be a general purpose library of order theoretic results.
-Instead, the definitions and theorems in `Lean.Order` are only intended as implementation details of the {keywordOf Lean.Parser.Command.declaration}`partial_fixpoint` feature, and they should be considered a private API that may change without notice.
+Instead, the definitions and theorems in {name}`Lean.Order` are only intended as implementation details of the {keywordOf Lean.Parser.Command.declaration}`partial_fixpoint` feature, and they should be considered a private API that may change without notice.
 
 The notion of a partial order, and that of a chain-complete partial order, are represented by the type classes {name}`Lean.Order.PartialOrder` and {name}`Lean.Order.CCPO`, respectively.
 
diff --git a/Manual/RecursiveDefs/WF.lean b/Manual/RecursiveDefs/WF.lean
index e05065a4b..5e46a6022 100644
--- a/Manual/RecursiveDefs/WF.lean
+++ b/Manual/RecursiveDefs/WF.lean
@@ -881,7 +881,7 @@ is not definitionally equal to the right-hand side
 n : Nat
 ⊢ div n 0 = 0
 ```
-However, using `WellFounded.fix_eq` to unfold the well-founded recursion, the three equations can be proved to hold:
+However, using {name}`WellFounded.fix_eq` to unfold the well-founded recursion, the three equations can be proved to hold:
 ```lean
 theorem div.eq0 : div n 0 = 0 := by
   unfold div
diff --git a/Manual/Simp.lean b/Manual/Simp.lean
index 4c7699264..f124485cb 100644
--- a/Manual/Simp.lean
+++ b/Manual/Simp.lean
@@ -36,7 +36,7 @@ Lean's simplifier can be invoked in a variety of ways.
 The most common patterns are captured in a set of tactics.
 The {ref "simp-tactics"}[tactic reference] contains a complete list of simplification tactics.
 
-Simplification tactics all contain `simp` in their name.
+Simplification tactics all contain {tactic}`simp` in their name.
 Aside from that, they are named according to a system of prefixes and suffixes that describe their functionality:
 
 : `-!` suffix
diff --git a/Manual/Tactics.lean b/Manual/Tactics.lean
index 80825c403..3ad385b24 100644
--- a/Manual/Tactics.lean
+++ b/Manual/Tactics.lean
@@ -572,7 +572,7 @@ example (n : Nat) : if n = 0 then n < 1 else n > 0 := by
 
 When pattern matching, instances of the {tech (key := "match discriminant")}[discriminant] in the goal are replaced with the patterns that match them in each branch.
 Each branch must then prove the refined goal.
-Compared to the `cases` tactic, using `match` can allow a greater degree of flexibility in the cases analysis being performed, but the requirement that each branch solve its goal completely makes it more difficult to incorporate into larger automation scripts.
+Compared to the {tactic}`cases` tactic, using {keywordOf Lean.Parser.Tactic.match}`match` can allow a greater degree of flexibility in the cases analysis being performed, but the requirement that each branch solve its goal completely makes it more difficult to incorporate into larger automation scripts.
 :::
 
 :::example "Reasoning by cases with `match`"
diff --git a/Manual/Tactics/Custom.lean b/Manual/Tactics/Custom.lean
index 1b0133f4c..cc1a48fa2 100644
--- a/Manual/Tactics/Custom.lean
+++ b/Manual/Tactics/Custom.lean
@@ -89,7 +89,7 @@ This is used to make a number of Lean's built-in tactics extensible—new behavi
 :::example "Extending {tactic}`trivial`"
 
 The {tactic}`trivial`, which is used by many other tactics to quickly dispatch subgoals that are not worth bothering the user with, is designed to be extended through new macro expansions.
-Lean's default {lean}`trivial` can't solve {lean}`IsEmpty []` goals:
+Lean's default {tactic}`trivial` can't solve {lean}`IsEmpty []` goals:
 ```lean
 def IsEmpty (xs : List α) : Prop :=
   ¬ xs ≠ []
diff --git a/Manual/Terms.lean b/Manual/Terms.lean
index 090545f91..535547f13 100644
--- a/Manual/Terms.lean
+++ b/Manual/Terms.lean
@@ -732,7 +732,7 @@ The use of field notation to apply other functions is called {deftech}_generaliz
 
 The identifier after the dot is looked up in the namespace of the term's type, which is the constant's name.
 If the type is not an application of a constant (e.g. a metavariable or a universe) then it doesn't have a namespace and generalized field notation cannot be used.
-As a special case, if an expression is a function, generalized field notation will look in the `Function` namespace. Therefore, {lean}`Nat.add.uncurry` is a use of generalized field notation that is equivalent to {lean}`Function.uncurry Nat.add`.
+As a special case, if an expression is a function, generalized field notation will look in the {name}`Function` namespace. Therefore, {lean}`Nat.add.uncurry` is a use of generalized field notation that is equivalent to {lean}`Function.uncurry Nat.add`.
 
 If the field is not found, but the constant can be unfolded to yield a further type which is a constant or application of a constant, then the process is repeated with the new constant.
 
diff --git a/Manual/Types.lean b/Manual/Types.lean
index 1c1b49ccb..3c60260da 100644
--- a/Manual/Types.lean
+++ b/Manual/Types.lean
@@ -30,7 +30,7 @@ Types can be thought of as denoting sets, while terms denote individual elements
 A term is {deftech}_well-typed_ if it has a type under the rules of Lean's type theory.
 Only well-typed terms have a meaning.
 
-Terms are a dependently typed λ-calculus: they include function abstraction, application, variables, and `let`-bindings.
+Terms are a dependently typed λ-calculus: they include function abstraction, application, variables, and {keywordOf Lean.Parser.Term.let}`let`-bindings.
 In addition to bound variables, variables in the term language may refer to {tech}[constructors], {tech}[type constructors], {tech}[recursors], {deftech}[defined constants], or opaque constants.
 Constructors, type constructors, recursors, and opaque constants are not subject to substitution, while defined constants may be replaced with their definitions.
 
@@ -477,7 +477,7 @@ universe $x:ident $xs:ident*
 
 Declares one or more universe variables for the extent of the current scope.
 
-Just as the `variable` command causes a particular identifier to be treated as a parameter with a particular type, the `universe` command causes the subsequent identifiers to be implicitly quantified as universe parameters in declarations that mention them, even if the option `autoImplicit` is {lean}`false`.
+Just as the {keywordOf Lean.Parser.Command.variable}`variable` command causes a particular identifier to be treated as a parameter with a particular type, the {keywordOf Lean.Parser.Command.universe}`universe` command causes the subsequent identifiers to be implicitly quantified as universe parameters in declarations that mention them, even if the option `autoImplicit` is {lean}`false`.
 :::
 
 :::Manual.example "The `universe` command when `autoImplicit` is `false`"
diff --git a/Manual/VCGen/Tutorial.lean b/Manual/VCGen/Tutorial.lean
index 17591abee..dabe029c8 100644
--- a/Manual/VCGen/Tutorial.lean
+++ b/Manual/VCGen/Tutorial.lean
@@ -668,7 +668,7 @@ The notation {lean}`⇓ r => Q' r` has the total interpretation, while {lean}`
 
 In the running example, {lean}`⦃P⦄ prog ⦃⇓ r => Q' r⦄` is unprovable, but {lean}`⦃P⦄ prog ⦃⇓? r => Q' r⦄` is trivially provable.
 However, the binary choice suggests that there is actually a _spectrum_ of correctness properties to express.
-The notion of postconditions {name}`PostCond` in `Std.Do` supports this spectrum.
+The notion of postconditions {name}`PostCond` in {namespace}`Std.Do` supports this spectrum.
 
 ::::