style: upgrade plain backticks to Verso semantic markup

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

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")

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}

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}
 

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}
 

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}
 

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
 %%%

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}

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.
 :::
 ::::
 

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 α

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) :=

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

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.]
 

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`.
 :::

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.

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.
 :::

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.

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