Indicating Substitutions for Theorem References in CalcCheck Hints

(You have read Getting Started with the CalcCheck Language and Getting Started with CalcCheckWeb.)

To document in more detail how a theorem mentioned in a hint is applied in that particular case, a substitution can be provided following the keyword with.

Example (if this does not display correctly, choose Unicode (UTF-8) character encoding in your browser):

Theorem (15.19): -(a + b) = (- a) + (- b)
Proof:
    -(a + b)
  =⟨ (15.20) with `a ≔ a + b` ⟩
    - 1 · (a + b)
  =⟨ “Distributivity of · over +” with `a, b, c ≔ - 1, a, b` ⟩
    - 1 · a + - 1 · b
  =⟨ (15.20) with `a ≔ a` ⟩
    - a + - 1 · b
  =⟨ (15.20) with `a ≔ b` ⟩
    - a + - b

Note:

1. There are spaces around with.
2. The substitution is surrounded by backquotes (`).

   On most keyboards, the backquote is in the upper left corner, on the same key as the tilde (~).

   Other quote-like characters will not work.

3. The use of backquotes here is following the MarkDown convention, according to which code pieces embedded in English sentences are surrounded by backquotes.
4. The substitution notation is that of LADM:
   variables ≔ expressions
   1. The variable list has the same length as the expression list.
   2. No variable occurs twice in the variable list.
   3. The “becomes” symbol ≔ is obtained via the symbol completion sequence \:= (backslash-colon-equal).
5. CalcCheckWeb notebooks labelled “with rigid matching” require all theorem variables to be substituted — otherwise, messages like “Rule variable `a` not substituted!” will be produced when checking these notebooks.