feat: mvcgen reference

.vale/styles/config/ignore/terms.txt

@@ -120,6 +120,7 @@ monoid
 monomorphic
 monomorphism
 morphism
+morphisms
 multipattern
 multipatterns
 multiset

Manual.lean

@@ -338,6 +338,9 @@ Eq
 HEq
 Max
 Min
+Std.Do
+Std.Do.PredTrans
+Std.Do.SVal
 Std.HashMap
 Std.ExtHashMap
 Std.DHashMap

Manual/Elaboration.lean

@@ -212,7 +212,7 @@ Instead, it provides low-level {tech}[recursors] that can be used to implement b
 Thus, the elaborator must translate definitions that use pattern matching and recursion into definitions that use recursors.{margin}[More details on the elaboration of recursive definitions is available in the {ref "recursive-definitions"}[dedicated section] on the topic.]
 This translation is additionally a proof that the function terminates for all potential arguments, because all functions that can be translated to recursors also terminate.
 
-The translation to recursors happens in two phases: during term elaboration, uses of pattern matching are replaced by appeals to {deftech}_auxiliary matching functions_ that implement the particular case distinction that occurs in the code.
+The translation to recursors happens in two phases: during term elaboration, uses of pattern matching are replaced by appeals to {deftech}_auxiliary matching functions_ (also referred to as {deftech}_matcher functions_) that implement the particular case distinction that occurs in the code.
 These auxiliary functions are themselves defined using recursors, though they do not make use of the recursors' ability to actually implement recursive behavior.{margin}[They use variants of the `casesOn` construction that is described in the {ref "recursor-elaboration-helpers"}[section on recursors and elaboration], specialized to reduce code size.]
 The term elaborator thus returns core-language terms in which pattern matching has been replaced with the use of special functions that implement case distinction, but these terms may still contain recursive occurrences of the function being defined.
 A definition that still includes recursion, but has otherwise been elaborated to the core language, is called a {deftech}[pre-definition].

Manual/Simp.lean

@@ -323,7 +323,7 @@ Prod.mk.injEq.{u, v} {α : Type u} {β : Type v} (fst : α) (snd : β) :
 :::::
 
 In addition to rewrite rules, {tactic}`simp` has a number of built-in reduction rules, {ref "simp-config"}[controlled by the `config` parameter].
-Even when the simp set is empty, {tactic}`simp` can replace `let`-bound variables with their values, reduce {keywordOf Lean.Parser.Term.match}`match` expressions whose scrutinees are constructor applications, reduce structure projections applied to constructors, or apply lambdas to their arguments.
+Even when the simp set is empty, {tactic}`simp` can replace `let`-bound variables with their values, reduce {keywordOf Lean.Parser.Term.match}`match` expressions whose {tech (key := "match discriminant")}[discriminants] are constructor applications, reduce structure projections applied to constructors, or apply lambdas to their arguments.
 
 # Simp sets
 %%%

Manual/Tactics.lean

@@ -570,13 +570,13 @@ example (n : Nat) : if n = 0 then n < 1 else n > 0 := by
 
 :::tactic Lean.Parser.Tactic.match (show := "match")
 
-When pattern matching, instances of the scrutinee in the goal are replaced with the patterns that match them in each branch.
+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.
 :::
 
 :::example "Reasoning by cases with `match`"
-In each branch of the {keywordOf Lean.Parser.Tactic.match}`match`, the scrutinee `n` has been replaced by either `0` or `k + 1`.
+In each branch of the {keywordOf Lean.Parser.Tactic.match}`match`, the discriminant `n` has been replaced by either `0` or `k + 1`.
 ```lean
 example (n : Nat) : if n = 0 then n < 1 else n > 0 := by
   match n with

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "795bc01672b6f616aeaa24a7c7c4b32b20fe9c04",
+   "rev": "c915ff13e15958681470dc2aa14ecd19500c900e",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",