RST backtick refactor (all *.rst except manual.rst and rst_examples.rst) (#17258)

Co-authored-by: quantimnot <quantimnot@users.noreply.github.com>

doc/drnim.rst

@@ -1,3 +1,5 @@
+.. default-role:: code
+
 ===================================
    DrNim User Guide
 ===================================
@@ -18,7 +20,7 @@ DrNim's command-line options are the same as the Nim compiler's.
 
 
 DrNim currently only checks the sections of your code that are marked
-via ``staticBoundChecks: on``:
+via `staticBoundChecks: on`:
 
 .. code-block:: nim
 
@@ -31,9 +33,9 @@ overflow errors are *not* prevented. Overflows will be checked for in
 the future.
 
 Later versions of the **Nim compiler** will **assume** that the checks inside
-the ``staticBoundChecks: on`` environment have been proven correct and so
+the `staticBoundChecks: on` environment have been proven correct and so
 it will **omit** the runtime checks. If you do not want this behavior, use
-instead ``{.push staticBoundChecks: defined(nimDrNim).}``. This way the
+instead `{.push staticBoundChecks: defined(nimDrNim).}`. This way the
 Nim compiler remains unaware of the performed proofs but DrNim will prove
 your code.
 
@@ -41,7 +43,7 @@ your code.
 Installation
 ============
 
-Run ``koch drnim``, the executable will afterwards be in ``$nim/bin/drnim``.
+Run `koch drnim`, the executable will afterwards be in `$nim/bin/drnim`.
 
 
 Motivating Example
@@ -67,7 +69,7 @@ detects it and produces the following error message::
 
   cannot prove: i <= len(a) + -1; counter example: i -> 0 a.len -> 0 [IndexCheck]
 
-In other words for ``i == 0`` and ``a.len == 0`` (for example!) there would be
+In other words for `i == 0` and `a.len == 0` (for example!) there would be
 an index out of bounds error.
 
 
@@ -82,37 +84,37 @@ DrNim adds 4 additional annotations (pragmas) to Nim:
 - `assume`:idx:
 
 These pragmas are ignored by the Nim compiler so that they don't have to
-be disabled via ``when defined(nimDrNim)``.
+be disabled via `when defined(nimDrNim)`.
 
 
 Invariant
 ---------
 
-An ``invariant`` is a proposition that must be true after every loop
+An `invariant` is a proposition that must be true after every loop
 iteration, it's tied to the loop body it's part of.
 
 
 Requires
 --------
 
-A ``requires`` annotation describes what the function expects to be true
-before it's called so that it can perform its operation. A ``requires``
+A `requires` annotation describes what the function expects to be true
+before it's called so that it can perform its operation. A `requires`
 annotation is also called a `precondition`:idx:.
 
 
 Ensures
 -------
 
-An ``ensures`` annotation describes what will be true after the function
-call. An ``ensures`` annotation is also called a `postcondition`:idx:.
+An `ensures` annotation describes what will be true after the function
+call. An `ensures` annotation is also called a `postcondition`:idx:.
 
 
 Assume
 ------
 
-An ``assume`` annotation describes what DrNim should **assume** to be true
+An `assume` annotation describes what DrNim should **assume** to be true
 in this section of the program. It is an unsafe escape mechanism comparable
-to Nim's ``cast`` statement. Use it only when you really know better
+to Nim's `cast` statement. Use it only when you really know better
 than DrNim. You should add a comment to a paper that proves the proposition
 you assume.
 
@@ -143,12 +145,12 @@ Example: insertionSort
 Unfortunately, the invariants required to prove that this code is correct take more
 code than the imperative instructions. However, this effort can be compensated
 by the fact that the result needs very little testing. Be aware though that
-DrNim only proves that after ``insertionSort`` this condition holds::
+DrNim only proves that after `insertionSort` this condition holds::
 
   forall(i in 1..<a.len, a[i-1] <= a[i])
 
 
-This is required, but not sufficient to describe that a ``sort`` operation
+This is required, but not sufficient to describe that a `sort` operation
 was performed. For example, the same postcondition is true for this proc
 which doesn't sort at all:
 
@@ -166,8 +168,8 @@ which doesn't sort at all:
 Syntax of propositions
 ======================
 
-The basic syntax is ``ensures|requires|invariant: <prop>``.
-A ``prop`` is either a comparison or a compound::
+The basic syntax is `ensures|requires|invariant: <prop>`.
+A `prop` is either a comparison or a compound::
 
   prop = nim_bool_expression
        | prop 'and' prop
@@ -186,17 +188,17 @@ A ``prop`` is either a comparison or a compound::
   quantifier = <new identifier> 'in' nim_iteration_expression
 
 
-``nim_iteration_expression`` here is an ordinary expression of Nim code
-that describes an iteration space, for example ``1..4`` or ``1..<a.len``.
+`nim_iteration_expression` here is an ordinary expression of Nim code
+that describes an iteration space, for example `1..4` or `1..<a.len`.
 
-``nim_bool_expression`` here is an ordinary expression of Nim code of
-type ``bool`` like ``a == 3`` or ``23 > a.len``.
+`nim_bool_expression` here is an ordinary expression of Nim code of
+type `bool` like `a == 3` or `23 > a.len`.
 
 The supported subset of Nim code that can be used in these expressions
-is currently underspecified but ``let`` variables, function parameters
-and ``result`` (which represents the function's final result) are amenable
+is currently underspecified but `let` variables, function parameters
+and `result` (which represents the function's final result) are amenable
 for verification. The expressions must not have any side-effects and must
 terminate.
 
-The operators ``forall``, ``exists``, ``->``, ``<->`` have to imported
-from ``std / logic``.
+The operators `forall`, `exists`, `->`, `<->` have to imported
+from `std / logic`.