From 56733b953eee491cbd1a95018bdb6a76506f5e61 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Thu, 23 Jan 2025 11:41:38 +0100
Subject: [PATCH] =?UTF-8?q?refactor:=20TerminationArgument=20=E2=86=92=20T?=
 =?UTF-8?q?erminationMeasure=20(#6727)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

this PR aligns the terminology of the code with the one use in the
reference manual, as developed with and refined by @david-christiansen.
---
 doc/declarations.md                           |   6 +-
 src/Lean/Elab/PreDefinition/Main.lean         |  16 +--
 .../PreDefinition/Structural/FindRecArg.lean  |  24 ++--
 .../Elab/PreDefinition/Structural/Main.lean   |  18 +--
 .../Elab/PreDefinition/TerminationHint.lean   |   2 +-
 ...nArgument.lean => TerminationMeasure.lean} |  42 +++----
 src/Lean/Elab/PreDefinition/WF/GuessLex.lean  | 114 +++++++++---------
 src/Lean/Elab/PreDefinition/WF/Main.lean      |  10 +-
 src/Lean/Elab/PreDefinition/WF/Rel.lean       |  28 ++---
 src/Lean/Meta/Match/MatcherApp/Transform.lean |   4 +-
 src/Lean/Parser/Term.lean                     |   8 +-
 tests/lean/decreasing_by.lean.expected.out    |   8 +-
 tests/lean/guessLex.lean                      |   8 +-
 tests/lean/guessLex.lean.expected.out         |  62 +++++-----
 tests/lean/guessLexDiff.lean.expected.out     |  16 +--
 tests/lean/guessLexFailures.lean.expected.out |  18 +--
 tests/lean/guessLexTricky.lean.expected.out   |   6 +-
 tests/lean/guessLexTricky2.lean.expected.out  |   4 +-
 tests/lean/issue2260.lean.expected.out        |   6 +-
 .../lean/mutwftypemismatch.lean.expected.out  |   8 +-
 tests/lean/run/issue4671.lean                 |   4 +-
 tests/lean/run/structuralMutual.lean          |   8 +-
 tests/lean/run/terminationByStructurally.lean |   6 +-
 .../lean/terminationFailure.lean.expected.out |   2 +-
 tests/lean/wf1.lean.expected.out              |   2 +-
 25 files changed, 215 insertions(+), 215 deletions(-)
 rename src/Lean/Elab/PreDefinition/{TerminationArgument.lean => TerminationMeasure.lean} (74%)

diff --git a/doc/declarations.md b/doc/declarations.md
index feb04e14d5..7a8c46a852 100644
--- a/doc/declarations.md
+++ b/doc/declarations.md
@@ -590,9 +590,9 @@ This table should be read as follows:
  * No other proofs were attempted, either because the parameter has a type without a non-trivial ``WellFounded`` instance (parameter 3), or because it is already clear that no decreasing measure can be found.
 
 
-Lean will print the termination argument it found if ``set_option showInferredTerminationBy true`` is set.
+Lean will print the termination measure it found if ``set_option showInferredTerminationBy true`` is set.
 
-If Lean does not find the termination argument, or if you want to be explicit, you can append a `termination_by` clause to the function definition, after the function's body, but before the `where` clause if present. It is of the form
+If Lean does not find the termination measure, or if you want to be explicit, you can append a `termination_by` clause to the function definition, after the function's body, but before the `where` clause if present. It is of the form
 ```
 termination_by e
 ```
@@ -672,7 +672,7 @@ def num_consts_lst : List Term → Nat
 end
 ```
 
-In a set of mutually recursive function, either all or no functions must have an explicit termination argument (``termination_by``). A change of the default termination tactic (``decreasing_by``) only affects the proofs about the recursive calls of that function, not the other functions in the group.
+In a set of mutually recursive function, either all or no functions must have an explicit termination measure (``termination_by``). A change of the default termination tactic (``decreasing_by``) only affects the proofs about the recursive calls of that function, not the other functions in the group.
 
 ```
 mutual
diff --git a/src/Lean/Elab/PreDefinition/Main.lean b/src/Lean/Elab/PreDefinition/Main.lean
index 082e834773..43fb159aab 100644
--- a/src/Lean/Elab/PreDefinition/Main.lean
+++ b/src/Lean/Elab/PreDefinition/Main.lean
@@ -219,14 +219,14 @@ def checkTerminationByHints (preDefs : Array PreDefinition) : CoreM Unit := do
         m!"`nontermination_partialFixpointursive`, so this one cannot be either.")
 
 /--
-Elaborates the `TerminationHint` in the clique to `TerminationArguments`
+Elaborates the `TerminationHint` in the clique to `TerminationMeasures`
 -/
-def elabTerminationByHints (preDefs : Array PreDefinition) : TermElabM (Array (Option TerminationArgument)) := do
+def elabTerminationByHints (preDefs : Array PreDefinition) : TermElabM (Array (Option TerminationMeasure)) := do
   preDefs.mapM fun preDef => do
     let arity ← lambdaTelescope preDef.value fun xs _ => pure xs.size
     let hints := preDef.termination
     hints.terminationBy?.mapM
-      (TerminationArgument.elab preDef.declName preDef.type arity hints.extraParams ·)
+      (TerminationMeasure.elab preDef.declName preDef.type arity hints.extraParams ·)
 
 def shouldUseStructural (preDefs : Array PreDefinition) : Bool :=
   preDefs.any fun preDef =>
@@ -279,18 +279,18 @@ def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLC
           try
             checkCodomainsLevel preDefs
             checkTerminationByHints preDefs
-            let termArg?s ← elabTerminationByHints preDefs
+            let termMeasures?s ← elabTerminationByHints preDefs
             if shouldUseStructural preDefs then
-              structuralRecursion preDefs termArg?s
+              structuralRecursion preDefs termMeasures?s
             else if shouldUsepartialFixpoint preDefs then
               partialFixpoint preDefs
             else if shouldUseWF preDefs then
-              wfRecursion preDefs termArg?s
+              wfRecursion preDefs termMeasures?s
             else
               withRef (preDefs[0]!.ref) <| mapError
                 (orelseMergeErrors
-                  (structuralRecursion preDefs termArg?s)
-                  (wfRecursion preDefs termArg?s))
+                  (structuralRecursion preDefs termMeasures?s)
+                  (wfRecursion preDefs termMeasures?s))
                 (fun msg =>
                   let preDefMsgs := preDefs.toList.map (MessageData.ofExpr $ mkConst ·.declName)
                   m!"fail to show termination for{indentD (MessageData.joinSep preDefMsgs Format.line)}\nwith errors\n{msg}")
diff --git a/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean b/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean
index 031af71cc6..4e70a4a496 100644
--- a/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Joachim Breitner
 -/
 prelude
-import Lean.Elab.PreDefinition.TerminationArgument
+import Lean.Elab.PreDefinition.TerminationMeasure
 import Lean.Elab.PreDefinition.Structural.Basic
 import Lean.Elab.PreDefinition.Structural.RecArgInfo
 
@@ -56,7 +56,7 @@ private def hasBadParamDep? (ys : Array Expr) (indParams : Array Expr) : MetaM (
 
 /--
 Assemble the `RecArgInfo` for the `i`th parameter in the parameter list `xs`. This performs
-various sanity checks on the argument (is it even an inductive type etc).
+various sanity checks on the parameter (is it even of inductive type etc).
 -/
 def getRecArgInfo (fnName : Name) (numFixed : Nat) (xs : Array Expr) (i : Nat) : MetaM RecArgInfo := do
   if h : i < xs.size then
@@ -112,17 +112,17 @@ considered.
 
 The `xs` are the fixed parameters, `value` the body with the fixed prefix instantiated.
 
-Takes the optional user annotations into account (`termArg?`). If this is given and the argument
+Takes the optional user annotation into account (`termMeasure?`). If this is given and the measure
 is unsuitable, throw an error.
 -/
 def getRecArgInfos (fnName : Name) (xs : Array Expr) (value : Expr)
-    (termArg? : Option TerminationArgument) : MetaM (Array RecArgInfo × MessageData) := do
+    (termMeasure? : Option TerminationMeasure) : MetaM (Array RecArgInfo × MessageData) := do
   lambdaTelescope value fun ys _ => do
-    if let .some termArg := termArg? then
-      -- User explicitly asked to use a certain argument, so throw errors eagerly
-      let recArgInfo ← withRef termArg.ref do
-        mapError (f := (m!"cannot use specified parameter for structural recursion:{indentD ·}")) do
-          getRecArgInfo fnName xs.size (xs ++ ys) (← termArg.structuralArg)
+    if let .some termMeasure := termMeasure? then
+      -- User explicitly asked to use a certain measure, so throw errors eagerly
+      let recArgInfo ← withRef termMeasure.ref do
+        mapError (f := (m!"cannot use specified measure for structural recursion:{indentD ·}")) do
+          getRecArgInfo fnName xs.size (xs ++ ys) (← termMeasure.structuralArg)
       return (#[recArgInfo], m!"")
     else
       let mut recArgInfos := #[]
@@ -233,12 +233,12 @@ def allCombinations (xss : Array (Array α)) : Option (Array (Array α)) :=
 
 
 def tryAllArgs (fnNames : Array Name) (xs : Array Expr) (values : Array Expr)
-   (termArg?s : Array (Option TerminationArgument)) (k : Array RecArgInfo → M α) : M α := do
+   (termMeasure?s : Array (Option TerminationMeasure)) (k : Array RecArgInfo → M α) : M α := do
   let mut report := m!""
   -- Gather information on all possible recursive arguments
   let mut recArgInfoss := #[]
-  for fnName in fnNames, value in values, termArg? in termArg?s do
-    let (recArgInfos, thisReport) ← getRecArgInfos fnName xs value termArg?
+  for fnName in fnNames, value in values, termMeasure? in termMeasure?s do
+    let (recArgInfos, thisReport) ← getRecArgInfos fnName xs value termMeasure?
     report := report ++ thisReport
     recArgInfoss := recArgInfoss.push recArgInfos
   -- Put non-indices first
diff --git a/src/Lean/Elab/PreDefinition/Structural/Main.lean b/src/Lean/Elab/PreDefinition/Structural/Main.lean
index d36f8e91a9..aad047ff18 100644
--- a/src/Lean/Elab/PreDefinition/Structural/Main.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/Main.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Joachim Breitner
 -/
 prelude
-import Lean.Elab.PreDefinition.TerminationArgument
+import Lean.Elab.PreDefinition.TerminationMeasure
 import Lean.Elab.PreDefinition.Structural.Basic
 import Lean.Elab.PreDefinition.Structural.FindRecArg
 import Lean.Elab.PreDefinition.Structural.Preprocess
@@ -127,7 +127,7 @@ private def elimMutualRecursion (preDefs : Array PreDefinition) (xs : Array Expr
   let valuesNew ← valuesNew.mapM (mkLambdaFVars xs ·)
   return (Array.zip preDefs valuesNew).map fun ⟨preDef, valueNew⟩ => { preDef with value := valueNew }
 
-private def inferRecArgPos (preDefs : Array PreDefinition) (termArg?s : Array (Option TerminationArgument)) :
+private def inferRecArgPos (preDefs : Array PreDefinition) (termMeasure?s : Array (Option TerminationMeasure)) :
     M (Array Nat × (Array PreDefinition) × Nat) := do
   withoutModifyingEnv do
     preDefs.forM (addAsAxiom ·)
@@ -142,7 +142,7 @@ private def inferRecArgPos (preDefs : Array PreDefinition) (termArg?s : Array (O
       assert! xs.size = maxNumFixed
       let values ← preDefs.mapM (instantiateLambda ·.value xs)
 
-      tryAllArgs fnNames xs values termArg?s fun recArgInfos => do
+      tryAllArgs fnNames xs values termMeasure?s fun recArgInfos => do
         let recArgPoss := recArgInfos.map (·.recArgPos)
         trace[Elab.definition.structural] "Trying argument set {recArgPoss}"
         let numFixed := recArgInfos.foldl (·.min ·.numFixed) maxNumFixed
@@ -156,20 +156,20 @@ private def inferRecArgPos (preDefs : Array PreDefinition) (termArg?s : Array (O
           let preDefs' ← elimMutualRecursion preDefs xs recArgInfos
           return (recArgPoss, preDefs', numFixed)
 
-def reportTermArg (preDef : PreDefinition) (recArgPos : Nat) : MetaM Unit := do
+def reporttermMeasure (preDef : PreDefinition) (recArgPos : Nat) : MetaM Unit := do
   if let some ref := preDef.termination.terminationBy?? then
     let fn ← lambdaTelescope preDef.value fun xs _ => mkLambdaFVars xs xs[recArgPos]!
-    let termArg : TerminationArgument:= {ref := .missing, structural := true, fn}
+    let termMeasure : TerminationMeasure:= {ref := .missing, structural := true, fn}
     let arity ← lambdaTelescope preDef.value fun xs _ => pure xs.size
-    let stx ← termArg.delab arity (extraParams := preDef.termination.extraParams)
+    let stx ← termMeasure.delab arity (extraParams := preDef.termination.extraParams)
     Tactic.TryThis.addSuggestion ref stx
 
 
-def structuralRecursion (preDefs : Array PreDefinition) (termArg?s : Array (Option TerminationArgument)) : TermElabM Unit := do
+def structuralRecursion (preDefs : Array PreDefinition) (termMeasure?s : Array (Option TerminationMeasure)) : TermElabM Unit := do
   let names := preDefs.map (·.declName)
-  let ((recArgPoss, preDefsNonRec, numFixed), state) ← run <| inferRecArgPos preDefs termArg?s
+  let ((recArgPoss, preDefsNonRec, numFixed), state) ← run <| inferRecArgPos preDefs termMeasure?s
   for recArgPos in recArgPoss, preDef in preDefs do
-    reportTermArg preDef recArgPos
+    reporttermMeasure preDef recArgPos
   state.addMatchers.forM liftM
   preDefsNonRec.forM fun preDefNonRec => do
     let preDefNonRec ← eraseRecAppSyntax preDefNonRec
diff --git a/src/Lean/Elab/PreDefinition/TerminationHint.lean b/src/Lean/Elab/PreDefinition/TerminationHint.lean
index 47725cf9a7..3dc6361c34 100644
--- a/src/Lean/Elab/PreDefinition/TerminationHint.lean
+++ b/src/Lean/Elab/PreDefinition/TerminationHint.lean
@@ -54,7 +54,7 @@ structure TerminationHints where
   Here we record the number of parameters past the `:`. It is set by
   `TerminationHints.rememberExtraParams` and used as follows:
 
-  * When we guess the termination argument in `GuessLex` and want to print it in surface-syntax
+  * When we guess the termination measure in `GuessLex` and want to print it in surface-syntax
     compatible form.
   * If there are fewer variables in the `termination_by` annotation than there are extra
     parameters, we know which parameters they should apply to (`TerminationBy.checkVars`).
diff --git a/src/Lean/Elab/PreDefinition/TerminationArgument.lean b/src/Lean/Elab/PreDefinition/TerminationMeasure.lean
similarity index 74%
rename from src/Lean/Elab/PreDefinition/TerminationArgument.lean
rename to src/Lean/Elab/PreDefinition/TerminationMeasure.lean
index 5998666b78..1d70811785 100644
--- a/src/Lean/Elab/PreDefinition/TerminationArgument.lean
+++ b/src/Lean/Elab/PreDefinition/TerminationMeasure.lean
@@ -14,8 +14,8 @@ import Lean.PrettyPrinter.Delaborator.Basic
 
 /-!
 This module contains
-* the data type `TerminationArgument`, the elaborated form of a `TerminationBy` clause,
-* the `TerminationArguments` type for a clique, and
+* the data type `TerminationMeasure`, the elaborated form of a `TerminationBy` clause,
+* the `TerminationMeasures` type for a clique, and
 * elaboration and deelaboration functions.
 -/
 
@@ -29,28 +29,28 @@ open Lean Meta Elab Term
 Elaborated form for a `termination_by` clause.
 
 The `fn` has the same (value) arity as the recursive functions (stored in
-`arity`), and maps its arguments (including fixed prefix, in unpacked form) to
-the termination argument.
+`arity`), and maps its measures (including fixed prefix, in unpacked form) to
+the termination measure.
 
-If `structural := Bool`, then the `fn` is a lambda picking out exactly one argument.
+If `structural := Bool`, then the `fn` is a lambda picking out exactly one measure.
 -/
-structure TerminationArgument where
+structure TerminationMeasure where
   ref : Syntax
   structural : Bool
   fn : Expr
 deriving Inhabited
 
-/-- A complete set of `TerminationArgument`s, as applicable to a single clique.  -/
-abbrev TerminationArguments := Array TerminationArgument
+/-- A complete set of `TerminationMeasure`s, as applicable to a single clique.  -/
+abbrev TerminationMeasures := Array TerminationMeasure
 
 /--
-Elaborates a `TerminationBy` to an `TerminationArgument`.
+Elaborates a `TerminationBy` to an `TerminationMeasure`.
 
 * `type` is the full type of the original recursive function, including fixed prefix.
 * `hint : TerminationBy` is the syntactic `TerminationBy`.
 -/
-def TerminationArgument.elab (funName : Name) (type : Expr) (arity extraParams : Nat)
-    (hint : TerminationBy) : TermElabM TerminationArgument := withDeclName funName do
+def TerminationMeasure.elab (funName : Name) (type : Expr) (arity extraParams : Nat)
+    (hint : TerminationBy) : TermElabM TerminationMeasure := withDeclName funName do
   assert! extraParams ≤ arity
 
   if h : hint.vars.size > extraParams then
@@ -73,7 +73,7 @@ def TerminationArgument.elab (funName : Name) (type : Expr) (arity extraParams :
         -- Structural recursion: The body has to be a single parameter, whose index we return
         if hint.structural then unless (ys ++ xs).contains body do
           let params := MessageData.andList ((ys ++ xs).toList.map (m!"'{·}'"))
-          throwErrorAt hint.ref m!"The termination argument of a structurally recursive " ++
+          throwErrorAt hint.ref m!"The termination measure of a structurally recursive " ++
             m!"function must be one of the parameters {params}, but{indentExpr body}\nisn't " ++
             m!"one of these."
 
@@ -87,24 +87,24 @@ def TerminationArgument.elab (funName : Name) (type : Expr) (arity extraParams :
     | 1 => "one parameter"
     | n => m!"{n} parameters"
 
-def TerminationArgument.structuralArg (termArg : TerminationArgument) : MetaM Nat := do
-  assert! termArg.structural
-  lambdaTelescope termArg.fn fun ys e => do
+def TerminationMeasure.structuralArg (measure : TerminationMeasure) : MetaM Nat := do
+  assert! measure.structural
+  lambdaTelescope measure.fn fun ys e => do
     let .some idx := ys.indexOf? e
-      | panic! "TerminationArgument.structuralArg: body not one of the parameters"
+      | panic! "TerminationMeasure.structuralArg: body not one of the parameters"
     return idx
 
 
 open PrettyPrinter Delaborator SubExpr Parser.Termination Parser.Term in
 /--
-Delaborates a `TerminationArgument` back to a `TerminationHint`, e.g. for `termination_by?`.
+Delaborates a `TerminationMeasure` back to a `TerminationHint`, e.g. for `termination_by?`.
 
 This needs extra information:
 * `arity` is the value arity of the recursive function
-* `extraParams` indicates how many of the functions arguments are bound “after the colon”.
+* `extraParams` indicates how many of the function's parameters are bound “after the colon”.
 -/
-def TerminationArgument.delab (arity : Nat) (extraParams : Nat) (termArg : TerminationArgument) : MetaM (TSyntax ``terminationBy) := do
-  lambdaBoundedTelescope termArg.fn (arity - extraParams) fun _ys e => do
+def TerminationMeasure.delab (arity : Nat) (extraParams : Nat) (measure : TerminationMeasure) : MetaM (TSyntax ``terminationBy) := do
+  lambdaBoundedTelescope measure.fn (arity - extraParams) fun _ys e => do
     pure (← delabCore e (delab := go extraParams #[])).1
   where
     go : Nat → TSyntaxArray `ident → DelabM (TSyntax ``terminationBy)
@@ -119,7 +119,7 @@ def TerminationArgument.delab (arity : Nat) (extraParams : Nat) (termArg : Termi
       -- drop trailing underscores
       let mut vars := vars
       while ! vars.isEmpty && vars.back!.raw.isOfKind ``hole do vars := vars.pop
-      if termArg.structural then
+      if measure.structural then
         if vars.isEmpty then
           `(terminationBy|termination_by structural $stxBody)
         else
diff --git a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean
index f8b0b60bf8..f15a7555ff 100644
--- a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean
+++ b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean
@@ -14,13 +14,13 @@ import Lean.Elab.Quotation
 import Lean.Elab.RecAppSyntax
 import Lean.Elab.PreDefinition.Basic
 import Lean.Elab.PreDefinition.Structural.Basic
-import Lean.Elab.PreDefinition.TerminationArgument
+import Lean.Elab.PreDefinition.TerminationMeasure
 import Lean.Elab.PreDefinition.WF.Basic
 import Lean.Data.Array
 
 
 /-!
-This module finds lexicographic termination arguments for well-founded recursion.
+This module finds lexicographic termination measures for well-founded recursion.
 
 Starting with basic measures (`sizeOf xᵢ` for all parameters `xᵢ`), and complex measures
 (e.g. `e₂ - e₁` if `e₁ < e₂` is found in the context of a recursive call) it tries all combinations
@@ -42,7 +42,7 @@ guessed lexicographic order.
 
 The following optimizations are applied to make this feasible:
 
-1. The crucial optimization is to look at each argument of each recursive call
+1. The crucial optimization is to look at each measure of each recursive call
    _once_, try to prove `<` and (if that fails `≤`), and then look at that table to
    pick a suitable measure.
 
@@ -50,7 +50,7 @@ The following optimizations are applied to make this feasible:
    expensive) tactics as few times as possible, while still being able to consider a possibly
    large number of combinations.
 
-3. Before we even try to prove `<`, we check if the arguments are equal (`=`). No well-founded
+3. Before we even try to prove `<`, we check if the measures are equal (`=`). No well-founded
    measure will relate equal terms, likely this check is faster than firing up the tactic engine,
    and it adds more signal to the output.
 
@@ -91,7 +91,7 @@ def originalVarNames (preDef : PreDefinition) : MetaM (Array Name) := do
 
 /--
 Given the original parameter names from `originalVarNames`, find
-good variable names to be used when talking about termination arguments:
+good variable names to be used when talking about termination measures:
 Use user-given parameter names if present; use x1...xn otherwise.
 
 The names ought to accessible (no macro scopes) and fresh wrt to the current environment,
@@ -121,7 +121,7 @@ def naryVarNames (xs : Array Name) : MetaM (Array Name) := do
         freshen ns (n.appendAfter "'")
 
 /-- A termination measure with extra fields for use within GuessLex -/
-structure Measure extends TerminationArgument where
+structure BasicMeasure extends TerminationMeasure where
   /--
   Like `.fn`, but unconditionally with `sizeOf` at the right type.
   We use this one when in `evalRecCall`
@@ -130,7 +130,7 @@ structure Measure extends TerminationArgument where
 deriving Inhabited
 
 /-- String description of this measure -/
-def Measure.toString (measure : Measure) : MetaM String := do
+def BasicMeasure.toString (measure : BasicMeasure) : MetaM String := do
   lambdaTelescope measure.fn fun _xs e => do
     -- This is a bit slopping if `measure.fn` takes more parameters than the `PreDefinition`
     return (← ppExpr e).pretty
@@ -138,10 +138,10 @@ def Measure.toString (measure : Measure) : MetaM String := do
 /--
 Determine if the measure for parameter `x` should be `sizeOf x` or just `x`.
 
-For non-mutual definitions, we omit `sizeOf` when the argument does not depend on
+For non-mutual definitions, we omit `sizeOf` when the measure does not depend on
 the other varying parameters, and its `WellFoundedRelation` instance goes via `SizeOf`.
 
-For mutual definitions, we omit `sizeOf` only when the argument is (at reducible transparency!) of
+For mutual definitions, we omit `sizeOf` only when the measure is (at reducible transparency!) of
 type `Nat` (else we'd have to worry about differently-typed measures from different functions to
 line up).
 -/
@@ -170,12 +170,12 @@ def withUserNames {α} (xs : Array Expr) (ns : Array Name) (k : MetaM α) : Meta
 
 /-- Create one measure for each (eligible) parameter of the given predefintion.  -/
 def simpleMeasures (preDefs : Array PreDefinition) (fixedPrefixSize : Nat)
-    (userVarNamess : Array (Array Name)) : MetaM (Array (Array Measure)) := do
+    (userVarNamess : Array (Array Name)) : MetaM (Array (Array BasicMeasure)) := do
   let is_mutual : Bool := preDefs.size > 1
   preDefs.mapIdxM fun funIdx preDef => do
     lambdaTelescope preDef.value fun xs _ => do
       withUserNames xs[fixedPrefixSize:] userVarNamess[funIdx]! do
-        let mut ret : Array Measure := #[]
+        let mut ret : Array BasicMeasure := #[]
         for x in xs[fixedPrefixSize:] do
           -- If the `SizeOf` instance produces a constant (e.g. because it's type is a `Prop` or
           -- `Type`), then ignore this parameter
@@ -369,7 +369,7 @@ def isNatCmp (e : Expr) : Option (Expr × Expr) :=
 
 def complexMeasures (preDefs : Array PreDefinition) (fixedPrefixSize : Nat)
     (userVarNamess : Array (Array Name)) (recCalls : Array RecCallWithContext) :
-    MetaM (Array (Array Measure)) := do
+    MetaM (Array (Array BasicMeasure)) := do
   preDefs.mapIdxM fun funIdx _preDef => do
     let mut measures := #[]
     for rc in recCalls do
@@ -426,7 +426,7 @@ def GuessLexRel.toNatRel : GuessLexRel → Expr
 For a given recursive call, and a choice of parameter and argument index,
 try to prove equality, < or ≤.
 -/
-def evalRecCall (decrTactic? : Option DecreasingBy) (callerMeasures calleeMeasures : Array Measure)
+def evalRecCall (decrTactic? : Option DecreasingBy) (callerMeasures calleeMeasures : Array BasicMeasure)
   (rcc : RecCallWithContext) (callerMeasureIdx calleeMeasureIdx : Nat) : MetaM GuessLexRel := do
   rcc.ctxt.run do
     let callerMeasure := callerMeasures[callerMeasureIdx]!
@@ -467,13 +467,13 @@ def evalRecCall (decrTactic? : Option DecreasingBy) (callerMeasures calleeMeasur
 /- A cache for `evalRecCall` -/
 structure RecCallCache where mk'' ::
   decrTactic? : Option DecreasingBy
-  callerMeasures : Array Measure
-  calleeMeasures : Array Measure
+  callerMeasures : Array BasicMeasure
+  calleeMeasures : Array BasicMeasure
   rcc : RecCallWithContext
   cache : IO.Ref (Array (Array (Option GuessLexRel)))
 
 /-- Create a cache to memoize calls to `evalRecCall descTactic? rcc` -/
-def RecCallCache.mk (decrTactics : Array (Option DecreasingBy)) (measuress : Array (Array Measure))
+def RecCallCache.mk (decrTactics : Array (Option DecreasingBy)) (measuress : Array (Array BasicMeasure))
     (rcc : RecCallWithContext) :
     BaseIO RecCallCache := do
   let decrTactic? := decrTactics[rcc.caller]!
@@ -499,7 +499,7 @@ def RecCallCache.prettyEntry (rcc : RecCallCache) (callerMeasureIdx calleeMeasur
   | .some rel => toString rel
   | .none => "_"
 
-/-- The measures that we order lexicographically can be comparing arguments,
+/-- The measures that we order lexicographically can be comparing basic measures,
 or numbering the functions -/
 inductive MutualMeasure where
   /-- For every function, the given argument index -/
@@ -509,9 +509,9 @@ inductive MutualMeasure where
 
 /-- Evaluate a recursive call at a given `MutualMeasure` -/
 def inspectCall (rc : RecCallCache) : MutualMeasure → MetaM GuessLexRel
-  | .args taIdxs => do
-    let callerMeasureIdx := taIdxs[rc.rcc.caller]!
-    let calleeMeasureIdx := taIdxs[rc.rcc.callee]!
+  | .args tmIdxs => do
+    let callerMeasureIdx := tmIdxs[rc.rcc.caller]!
+    let calleeMeasureIdx := tmIdxs[rc.rcc.callee]!
     rc.eval callerMeasureIdx calleeMeasureIdx
   | .func funIdx => do
     if rc.rcc.caller == funIdx && rc.rcc.callee != funIdx then
@@ -554,16 +554,16 @@ where
 /--
 Enumerate all measures we want to try.
 
-All arguments (resp. combinations thereof) and
+All measures (resp. combinations thereof) and
 possible orderings of functions (if more than one)
 -/
-def generateMeasures (numTermArgs : Array Nat) : MetaM (Array MutualMeasure) := do
-  let some arg_measures := generateCombinations? numTermArgs
+def generateMeasures (numMeasures : Array Nat) : MetaM (Array MutualMeasure) := do
+  let some arg_measures := generateCombinations? numMeasures
       | throwError "Too many combinations"
 
   let func_measures :=
-    if numTermArgs.size > 1 then
-      (List.range numTermArgs.size).toArray
+    if numMeasures.size > 1 then
+      (List.range numMeasures.size).toArray
     else
       #[]
 
@@ -652,8 +652,8 @@ def RecCallWithContext.posString (rcc : RecCallWithContext) : MetaM String := do
   return s!"{position.line}:{position.column}{endPosStr}"
 
 
-/-- How to present the measure in the table header, possibly abbreviated. -/
-def measureHeader (measure : Measure) : StateT (Nat × String) MetaM String := do
+/-- How to present the basic measure in the table header, possibly abbreviated. -/
+def measureHeader (measure : BasicMeasure) : StateT (Nat × String) MetaM String := do
   let s ← measure.toString
   if s.length > 5 then
     let (i, footer) ← get
@@ -670,7 +670,7 @@ def collectHeaders {α} (a : StateT (Nat × String) MetaM α) : MetaM (α × Str
 
 
 /-- Explain what we found out about the recursive calls (non-mutual case) -/
-def explainNonMutualFailure (measures : Array Measure) (rcs : Array RecCallCache) : MetaM Format := do
+def explainNonMutualFailure (measures : Array BasicMeasure) (rcs : Array RecCallCache) : MetaM Format := do
   let (header, footer) ← collectHeaders (measures.mapM measureHeader)
   let mut table : Array (Array String) := #[#[""] ++ header]
   for i in [:rcs.size], rc in rcs do
@@ -685,7 +685,7 @@ def explainNonMutualFailure (measures : Array Measure) (rcs : Array RecCallCache
     return out ++ "\n\n" ++ footer
 
 /-- Explain what we found out about the recursive calls (mutual case) -/
-def explainMutualFailure (declNames : Array Name) (measuress : Array (Array Measure))
+def explainMutualFailure (declNames : Array Name) (measuress : Array (Array BasicMeasure))
     (rcs : Array RecCallCache) : MetaM Format := do
   let (headerss, footer) ← collectHeaders (measuress.mapM (·.mapM measureHeader))
 
@@ -718,9 +718,9 @@ def explainMutualFailure (declNames : Array Name) (measuress : Array (Array Meas
 
   return r
 
-def explainFailure (declNames : Array Name) (measuress : Array (Array Measure))
+def explainFailure (declNames : Array Name) (measuress : Array (Array BasicMeasure))
     (rcs : Array RecCallCache) : MetaM Format := do
-  let mut r : Format := "The arguments relate at each recursive call as follows:\n" ++
+  let mut r : Format := "The basic measures relate at each recursive call as follows:\n" ++
     "(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)\n"
   if declNames.size = 1 then
     r := r ++ (← explainNonMutualFailure measuress[0]! rcs)
@@ -739,29 +739,29 @@ def mkProdElem (xs : Array Expr) : MetaM Expr := do
     let n := xs.size
     xs[0:n-1].foldrM (init:=xs[n-1]!) fun x p => mkAppM ``Prod.mk #[x,p]
 
-def toTerminationArguments (preDefs : Array PreDefinition) (fixedPrefixSize : Nat)
-    (userVarNamess : Array (Array Name)) (measuress : Array (Array Measure))
-    (solution : Array MutualMeasure) : MetaM TerminationArguments := do
+def toTerminationMeasures (preDefs : Array PreDefinition) (fixedPrefixSize : Nat)
+    (userVarNamess : Array (Array Name)) (measuress : Array (Array BasicMeasure))
+    (solution : Array MutualMeasure) : MetaM TerminationMeasures := do
   preDefs.mapIdxM fun funIdx preDef => do
     let measures := measuress[funIdx]!
     lambdaTelescope preDef.value fun xs _ => do
       withUserNames xs[fixedPrefixSize:] userVarNamess[funIdx]! do
         let args := solution.map fun
-          | .args taIdxs => measures[taIdxs[funIdx]!]!.fn.beta xs
+          | .args tmIdxs => measures[tmIdxs[funIdx]!]!.fn.beta xs
           | .func funIdx' => mkNatLit <| if funIdx' == funIdx then 1 else 0
         let fn ← mkLambdaFVars xs (← mkProdElem args)
         return { ref := .missing, structural := false, fn}
 
 /--
-Shows the inferred termination argument to the user, and implements `termination_by?`
+Shows the inferred termination measure to the user, and implements `termination_by?`
 -/
-def reportTermArgs (preDefs : Array PreDefinition) (termArgs : TerminationArguments) : MetaM Unit := do
-  for preDef in preDefs, termArg in termArgs do
+def reportTerminationMeasures (preDefs : Array PreDefinition) (termMeasures : TerminationMeasures) : MetaM Unit := do
+  for preDef in preDefs, termMeasure in termMeasures do
     let stx := do
       let arity ← lambdaTelescope preDef.value fun xs _ => pure xs.size
-      termArg.delab arity (extraParams := preDef.termination.extraParams)
+      termMeasure.delab arity (extraParams := preDef.termination.extraParams)
     if showInferredTerminationBy.get (← getOptions) then
-      logInfoAt preDef.ref m!"Inferred termination argument:\n{← stx}"
+      logInfoAt preDef.ref m!"Inferred termination measure:\n{← stx}"
     if let some ref := preDef.termination.terminationBy?? then
       Tactic.TryThis.addSuggestion ref (← stx)
 
@@ -771,14 +771,14 @@ open GuessLex
 /--
 Main entry point of this module:
 
-Try to find a lexicographic ordering of the arguments for which the recursive definition
+Try to find a lexicographic ordering of the basic measures for which the recursive definition
 terminates. See the module doc string for a high-level overview.
 
-The `preDefs` are used to determine arity and types of arguments; the bodies are ignored.
+The `preDefs` are used to determine arity and types of parameters; the bodies are ignored.
 -/
 def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition)
     (fixedPrefixSize : Nat) (argsPacker : ArgsPacker) :
-    MetaM TerminationArguments := do
+    MetaM TerminationMeasures := do
   let userVarNamess ← argsPacker.varNamess.mapM (naryVarNames ·)
   trace[Elab.definition.wf] "varNames is: {userVarNamess}"
 
@@ -788,30 +788,30 @@ def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition)
 
   -- For every function, the measures we want to use
   -- (One for each non-forbiddend arg)
-  let meassures₁ ← simpleMeasures preDefs fixedPrefixSize userVarNamess
-  let meassures₂ ← complexMeasures preDefs fixedPrefixSize userVarNamess recCalls
-  let measuress := Array.zipWith meassures₁ meassures₂ (· ++ ·)
+  let basicMeassures₁ ← simpleMeasures preDefs fixedPrefixSize userVarNamess
+  let basicMeassures₂ ← complexMeasures preDefs fixedPrefixSize userVarNamess recCalls
+  let basicMeasures := Array.zipWith basicMeassures₁ basicMeassures₂ (· ++ ·)
 
   -- The list of measures, including the measures that order functions.
   -- The function ordering measures come last
-  let measures ← generateMeasures (measuress.map (·.size))
+  let mutualMeasures ← generateMeasures (basicMeasures.map (·.size))
 
   -- If there is only one plausible measure, use that
-  if let #[solution] := measures then
-    let termArgs ← toTerminationArguments preDefs fixedPrefixSize userVarNamess measuress #[solution]
-    reportTermArgs preDefs termArgs
-    return termArgs
+  if let #[solution] := mutualMeasures then
+    let termMeasures ← toTerminationMeasures preDefs fixedPrefixSize userVarNamess basicMeasures #[solution]
+    reportTerminationMeasures preDefs termMeasures
+    return termMeasures
 
-  let rcs ← recCalls.mapM (RecCallCache.mk (preDefs.map (·.termination.decreasingBy?)) measuress ·)
+  let rcs ← recCalls.mapM (RecCallCache.mk (preDefs.map (·.termination.decreasingBy?)) basicMeasures ·)
   let callMatrix := rcs.map (inspectCall ·)
 
-  match ← liftMetaM <| solve measures callMatrix with
+  match ← liftMetaM <| solve mutualMeasures callMatrix with
   | .some solution => do
-    let termArgs ← toTerminationArguments preDefs fixedPrefixSize userVarNamess measuress solution
-    reportTermArgs preDefs termArgs
-    return termArgs
+    let termMeasures ← toTerminationMeasures preDefs fixedPrefixSize userVarNamess basicMeasures solution
+    reportTerminationMeasures preDefs termMeasures
+    return termMeasures
   | .none =>
-    let explanation ← explainFailure (preDefs.map (·.declName)) measuress rcs
+    let explanation ← explainFailure (preDefs.map (·.declName)) basicMeasures rcs
     Lean.throwError <| "Could not find a decreasing measure.\n" ++
       explanation ++ "\n" ++
       "Please use `termination_by` to specify a decreasing measure."
diff --git a/src/Lean/Elab/PreDefinition/WF/Main.lean b/src/Lean/Elab/PreDefinition/WF/Main.lean
index ab5eede9a8..952770b637 100644
--- a/src/Lean/Elab/PreDefinition/WF/Main.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Main.lean
@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Elab.PreDefinition.Basic
-import Lean.Elab.PreDefinition.TerminationArgument
+import Lean.Elab.PreDefinition.TerminationMeasure
 import Lean.Elab.PreDefinition.Mutual
 import Lean.Elab.PreDefinition.WF.PackMutual
 import Lean.Elab.PreDefinition.WF.Preprocess
@@ -19,8 +19,8 @@ namespace Lean.Elab
 open WF
 open Meta
 
-def wfRecursion (preDefs : Array PreDefinition) (termArg?s : Array (Option TerminationArgument)) : TermElabM Unit := do
-  let termArgs? := termArg?s.mapM id -- Either all or none, checked by `elabTerminationByHints`
+def wfRecursion (preDefs : Array PreDefinition) (termMeasure?s : Array (Option TerminationMeasure)) : TermElabM Unit := do
+  let termMeasures? := termMeasure?s.mapM id -- Either all or none, checked by `elabTerminationByHints`
   let preDefs ← preDefs.mapM fun preDef =>
     return { preDef with value := (← preprocess preDef.value) }
   let (fixedPrefixSize, argsPacker, unaryPreDef) ← withoutModifyingEnv do
@@ -36,8 +36,8 @@ def wfRecursion (preDefs : Array PreDefinition) (termArg?s : Array (Option Termi
     let preDefsDIte ← preDefs.mapM fun preDef => return { preDef with value := (← iteToDIte preDef.value) }
     return (fixedPrefixSize, argsPacker, ← packMutual fixedPrefixSize argsPacker preDefsDIte)
 
-  let wf : TerminationArguments ← do
-    if let some tas := termArgs? then pure tas else
+  let wf : TerminationMeasures ← do
+    if let some tms := termMeasures? then pure tms else
     -- No termination_by here, so use GuessLex to infer one
     guessLex preDefs unaryPreDef fixedPrefixSize argsPacker
 
diff --git a/src/Lean/Elab/PreDefinition/WF/Rel.lean b/src/Lean/Elab/PreDefinition/WF/Rel.lean
index 5bb6dcecda..5b14e2ce02 100644
--- a/src/Lean/Elab/PreDefinition/WF/Rel.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Rel.lean
@@ -9,7 +9,7 @@ import Lean.Meta.Tactic.Cases
 import Lean.Meta.Tactic.Rename
 import Lean.Elab.SyntheticMVars
 import Lean.Elab.PreDefinition.Basic
-import Lean.Elab.PreDefinition.TerminationArgument
+import Lean.Elab.PreDefinition.TerminationMeasure
 import Lean.Meta.ArgsPacker
 
 namespace Lean.Elab.WF
@@ -17,21 +17,21 @@ open Meta
 open Term
 
 /--
-The termination arguments must not depend on the varying parameters of the function, and in
+The termination measures must not depend on the varying parameters of the function, and in
 a mutual clique, they must be the same for all functions.
 
 This ensures the preconditions for `ArgsPacker.uncurryND`.
 -/
 def checkCodomains (names : Array Name) (prefixArgs : Array Expr) (arities : Array Nat)
-    (termArgs : TerminationArguments) : TermElabM Expr := do
+    (termMeasures : TerminationMeasures) : TermElabM Expr := do
   let mut codomains := #[]
-  for name in names, arity in arities, termArg in termArgs do
-    let type ← inferType (termArg.fn.beta prefixArgs)
+  for name in names, arity in arities, termMeasure in termMeasures do
+    let type ← inferType (termMeasure.fn.beta prefixArgs)
     let codomain ← forallBoundedTelescope type arity fun xs codomain => do
       let fvars := xs.map (·.fvarId!)
       if codomain.hasAnyFVar (fvars.contains ·) then
-        throwErrorAt termArg.ref  m!"The termination argument's type must not depend on the " ++
-          m!"function's varying parameters, but {name}'s termination argument does:{indentExpr type}\n" ++
+        throwErrorAt termMeasure.ref  m!"The termination measure's type must not depend on the " ++
+          m!"function's varying parameters, but {name}'s termination measure does:{indentExpr type}\n" ++
           "Try using `sizeOf` explicitly"
       pure codomain
     codomains := codomains.push codomain
@@ -39,26 +39,26 @@ def checkCodomains (names : Array Name) (prefixArgs : Array Expr) (arities : Arr
   let codomain0 := codomains[0]!
   for h : i in [1 : codomains.size] do
     unless ← isDefEqGuarded codomain0 codomains[i] do
-      throwErrorAt termArgs[i]!.ref m!"The termination arguments of mutually recursive functions " ++
-        m!"must have the same return type, but the termination argument of {names[0]!} has type" ++
+      throwErrorAt termMeasures[i]!.ref m!"The termination measures of mutually recursive functions " ++
+        m!"must have the same return type, but the termination measure of {names[0]!} has type" ++
         m!"{indentExpr codomain0}\n" ++
-        m!"while the termination argument of {names[i]!} has type{indentExpr codomains[i]}\n" ++
+        m!"while the termination measure of {names[i]!} has type{indentExpr codomains[i]}\n" ++
         "Try using `sizeOf` explicitly"
   return codomain0
 
 /--
-If the `termArgs` map the packed argument `argType` to `β`, then this function passes to the
+If the `termMeasures` map the packed argument `argType` to `β`, then this function passes to the
 continuation a value of type `WellFoundedRelation argType` that is derived from the instance
 for `WellFoundedRelation β` using `invImage`.
 -/
 def elabWFRel (declNames : Array Name) (unaryPreDefName : Name) (prefixArgs : Array Expr)
-    (argsPacker : ArgsPacker) (argType : Expr) (termArgs : TerminationArguments)
+    (argsPacker : ArgsPacker) (argType : Expr) (termMeasures : TerminationMeasures)
     (k : Expr → TermElabM α) : TermElabM α := withDeclName unaryPreDefName do
   let α := argType
   let u ← getLevel α
-  let β ← checkCodomains declNames prefixArgs argsPacker.arities termArgs
+  let β ← checkCodomains declNames prefixArgs argsPacker.arities termMeasures
   let v ← getLevel β
-  let packedF ← argsPacker.uncurryND (termArgs.map (·.fn.beta prefixArgs))
+  let packedF ← argsPacker.uncurryND (termMeasures.map (·.fn.beta prefixArgs))
   let inst ← synthInstance (.app (.const ``WellFoundedRelation [v]) β)
   let rel ← instantiateMVars (mkApp4 (.const ``invImage [u,v]) α β packedF inst)
   k rel
diff --git a/src/Lean/Meta/Match/MatcherApp/Transform.lean b/src/Lean/Meta/Match/MatcherApp/Transform.lean
index 92cfeccf5f..9af30b1273 100644
--- a/src/Lean/Meta/Match/MatcherApp/Transform.lean
+++ b/src/Lean/Meta/Match/MatcherApp/Transform.lean
@@ -50,8 +50,8 @@ private partial def updateAlts (unrefinedArgType : Expr) (typeNew : Expr) (altNu
   - each alternative is a lambda abstraction where `ys_i.size == matcherApp.altNumParams[i]`
 
   This is used in `Lean.Elab.PreDefinition.WF.Fix` when replacing recursive calls with calls to
-  the argument provided by `fix` to refine the termination argument, which may mention `major`.
-  See there for how to use this function.
+  the argument provided by `fix` to refine type of the local variable used for recursive calls,
+  which may mention `major`. See there for how to use this function.
 -/
 def addArg (matcherApp : MatcherApp) (e : Expr) : MetaM MatcherApp :=
   lambdaTelescope matcherApp.motive fun motiveArgs motiveBody => do
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index fad0247f99..dcf15abba6 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -692,7 +692,7 @@ letrec we need them here already.
 -/
 
 /--
-Specify a termination argument for recursive functions.
+Specify a termination measure for recursive functions.
 ```
 termination_by a - b
 ```
@@ -710,8 +710,8 @@ recursion. The syntax `termination_by structural a` (or `termination_by structur
 indicates the function is expected to be structural recursive on the argument. In this case
 the body of the `termination_by` clause must be one of the function's parameters.
 
-If omitted, a termination argument will be inferred. If written as `termination_by?`,
-the inferrred termination argument will be suggested.
+If omitted, a termination measure will be inferred. If written as `termination_by?`,
+the inferrred termination measure will be suggested.
 
 -/
 @[builtin_doc] def terminationBy := leading_parser
@@ -751,7 +751,7 @@ the syntax `partial_fixpoint monotonicity by $tac` the proof can be done manuall
               checkColGt "indented monotonicity proof" >> termParser))
 
 /--
-Manually prove that the termination argument (as specified with `termination_by` or inferred)
+Manually prove that the termination measure (as specified with `termination_by` or inferred)
 decreases at each recursive call.
 
 By default, the tactic `decreasing_tactic` is used.
diff --git a/tests/lean/decreasing_by.lean.expected.out b/tests/lean/decreasing_by.lean.expected.out
index d1f488065d..474a642aa8 100644
--- a/tests/lean/decreasing_by.lean.expected.out
+++ b/tests/lean/decreasing_by.lean.expected.out
@@ -1,12 +1,12 @@
 decreasing_by.lean:34:0-39:17: error: Could not find a decreasing measure.
-The arguments relate at each recursive call as follows:
+The basic measures relate at each recursive call as follows:
 (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
             n m
 1) 34:29-43 = ?
 2) 34:46-62 ? _
 Please use `termination_by` to specify a decreasing measure.
 decreasing_by.lean:61:0-67:19: error: Could not find a decreasing measure.
-The arguments relate at each recursive call as follows:
+The basic measures relate at each recursive call as follows:
 (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
             n m
 1) 61:29-43 = ?
@@ -27,7 +27,7 @@ n m : Nat
 n m : Nat
 ⊢ Prod.Lex (fun a₁ a₂ => a₁ < a₂) (fun a₁ a₂ => a₁ < a₂) (dec1 n, 100) (n, m)
 decreasing_by.lean:93:0-94:22: error: Could not find a decreasing measure.
-The arguments relate at each recursive call as follows:
+The basic measures relate at each recursive call as follows:
 (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
             n m
 1) 93:29-43 = ?
@@ -37,7 +37,7 @@ decreasing_by.lean:104:0-106:17: error: unsolved goals
 n m : Nat
 ⊢ Prod.Lex (fun a₁ a₂ => a₁ < a₂) (fun a₁ a₂ => a₁ < a₂) (dec1 n, 100) (n, m)
 decreasing_by.lean:114:0-117:17: error: Could not find a decreasing measure.
-The arguments relate at each recursive call as follows:
+The basic measures relate at each recursive call as follows:
 (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
              n m
 1) 114:29-43 = ?
diff --git a/tests/lean/guessLex.lean b/tests/lean/guessLex.lean
index 7917434fcb..44df94ae12 100644
--- a/tests/lean/guessLex.lean
+++ b/tests/lean/guessLex.lean
@@ -90,7 +90,7 @@ def confuseLex2 : @PSigma Nat (fun _ => Nat) → Nat
   | ⟨0,_⟩ => 0
   | ⟨.succ y,.succ n⟩ => confuseLex2 ⟨y,n⟩
 
--- NB: uses sizeOf to make the termination argument non-dependent
+-- NB: uses sizeOf to make the termination measure non-dependent
 def dependent : (n : Nat) → (m : Fin n) → Nat
  | 0, i => Fin.elim0 i
  | .succ 0, 0 => 0
@@ -137,7 +137,7 @@ def shadow2 (some_n : Nat) : Nat → Nat
   | .succ n => shadow2 (some_n + 1) n
 decreasing_by decreasing_tactic
 
--- Tests that the inferred termination argument is shown without extra underscores
+-- Tests that the inferred termination measure is shown without extra underscores
 def foo : Nat → Nat → Nat → Nat
   | _, 0, acc => acc
   | k, n+1, acc => foo (k+1) n (acc + k)
@@ -181,7 +181,7 @@ end VarNames
 namespace MutualNotNat1
 
 -- A type that isn't Nat, checking that the inferred argument uses `sizeOf` so that
--- the types of the termination argument aligns.
+-- the types of the termination measure aligns.
 structure OddNat2 where nat : Nat
 instance : SizeOf OddNat2 := ⟨fun n => n.nat⟩
 @[simp] theorem  OddNat2.sizeOf_eq (n : OddNat2) : sizeOf n = n.nat := rfl
@@ -197,7 +197,7 @@ end MutualNotNat1
 
 namespace MutualNotNat2
 -- A type that is defeq to Nat, but with a different `sizeOf`, checking that the
--- inferred argument uses `sizeOf` so that the types of the termination argument aligns.
+-- inferred argument uses `sizeOf` so that the types of the termination measure aligns.
 def OddNat3 := Nat
 instance : SizeOf OddNat3 := ⟨fun n => 42 - @id Nat n⟩
 @[simp] theorem  OddNat3.sizeOf_eq (n : OddNat3) : sizeOf n = 42 - @id Nat n := rfl
diff --git a/tests/lean/guessLex.lean.expected.out b/tests/lean/guessLex.lean.expected.out
index f584037118..f5c8f9302d 100644
--- a/tests/lean/guessLex.lean.expected.out
+++ b/tests/lean/guessLex.lean.expected.out
@@ -1,62 +1,62 @@
-Inferred termination argument:
+Inferred termination measure:
 termination_by (n, m)
-Inferred termination argument:
+Inferred termination measure:
 termination_by (m, n)
-Inferred termination argument:
+Inferred termination measure:
 termination_by (n, m)
-Inferred termination argument:
+Inferred termination measure:
 termination_by x1 x2 => (x2, x1)
-Inferred termination argument:
+Inferred termination measure:
 termination_by x1 => x1
-Inferred termination argument:
+Inferred termination measure:
 termination_by x1 => x1
-Inferred termination argument:
+Inferred termination measure:
 termination_by x1 => x1
-Inferred termination argument:
+Inferred termination measure:
 termination_by x1 => x1
-Inferred termination argument:
+Inferred termination measure:
 termination_by x1 => (x1, 0)
-Inferred termination argument:
+Inferred termination measure:
 termination_by (n, 1)
-Inferred termination argument:
+Inferred termination measure:
 termination_by (m, n)
-Inferred termination argument:
+Inferred termination measure:
 termination_by x1 x2 x3 x4 x5 x6 x7 x8 => (x8, x7, x6, x5, x4, x3, x2, x1)
-Inferred termination argument:
+Inferred termination measure:
 termination_by x1 => x1
-Inferred termination argument:
+Inferred termination measure:
 termination_by x1 => sizeOf x1
-Inferred termination argument:
+Inferred termination measure:
 termination_by n m => (n, sizeOf m)
-Inferred termination argument:
+Inferred termination measure:
 termination_by m => m
-Inferred termination argument:
+Inferred termination measure:
 termination_by (sizeOf a, 1)
-Inferred termination argument:
+Inferred termination measure:
 termination_by (sizeOf a, 0)
-Inferred termination argument:
+Inferred termination measure:
 termination_by x2' => x2'
-Inferred termination argument:
+Inferred termination measure:
 termination_by x2 => x2
-Inferred termination argument:
+Inferred termination measure:
 termination_by _ x2 => x2
-Inferred termination argument:
+Inferred termination measure:
 termination_by x1 => sizeOf x1
-Inferred termination argument:
+Inferred termination measure:
 termination_by x2 => SizeOf.sizeOf x2
-Inferred termination argument:
+Inferred termination measure:
 termination_by x1 => SizeOf.sizeOf x1
-Inferred termination argument:
+Inferred termination measure:
 termination_by x2 => SizeOf.sizeOf x2
-Inferred termination argument:
+Inferred termination measure:
 termination_by x1 => x1
-Inferred termination argument:
+Inferred termination measure:
 termination_by x1 => sizeOf x1
-Inferred termination argument:
+Inferred termination measure:
 termination_by x1 => x1
-Inferred termination argument:
+Inferred termination measure:
 termination_by sizeOf o
-Inferred termination argument:
+Inferred termination measure:
 termination_by x1 => x1
-Inferred termination argument:
+Inferred termination measure:
 termination_by x1 => sizeOf x1
diff --git a/tests/lean/guessLexDiff.lean.expected.out b/tests/lean/guessLexDiff.lean.expected.out
index 7abee8bc37..2b017593ba 100644
--- a/tests/lean/guessLexDiff.lean.expected.out
+++ b/tests/lean/guessLexDiff.lean.expected.out
@@ -1,14 +1,14 @@
-Inferred termination argument:
+Inferred termination measure:
 termination_by n - i
-Inferred termination argument:
+Inferred termination measure:
 termination_by xs.size - i
-Inferred termination argument:
+Inferred termination measure:
 termination_by xs.size - i
-Inferred termination argument:
+Inferred termination measure:
 termination_by (xs.size - i, ys.size - j)
-Inferred termination argument:
+Inferred termination measure:
 termination_by (xs.size - i, i - j)
-Inferred termination argument:
+Inferred termination measure:
 termination_by (xs.size - i, i)
 guessLexDiff.lean:84:4-84:11: error: fail to show termination for
   failure
@@ -22,7 +22,7 @@ Cannot use parameter i:
 
 
 Could not find a decreasing measure.
-The arguments relate at each recursive call as follows:
+The basic measures relate at each recursive call as follows:
 (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
             i #1 #2 i + i
 1) 85:26-38 =  =  =     =
@@ -54,7 +54,7 @@ Cannot use parameters i of mutual_failure and i of mutual_failure2:
 
 
 Could not find a decreasing measure.
-The arguments relate at each recursive call as follows:
+The basic measures relate at each recursive call as follows:
 (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
 Call from mutual_failure to mutual_failure2 at 104:4-24:
    i #1 #2
diff --git a/tests/lean/guessLexFailures.lean.expected.out b/tests/lean/guessLexFailures.lean.expected.out
index e159fd9263..8cd0d6ffd6 100644
--- a/tests/lean/guessLexFailures.lean.expected.out
+++ b/tests/lean/guessLexFailures.lean.expected.out
@@ -11,13 +11,13 @@ Cannot use parameter #2:
 
 
 Could not find a decreasing measure.
-The arguments relate at each recursive call as follows:
+The basic measures relate at each recursive call as follows:
 (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
             x1 x2
 1) 11:12-46  ?  ?
 Please use `termination_by` to specify a decreasing measure.
 guessLexFailures.lean:15:0-18:31: error: Could not find a decreasing measure.
-The arguments relate at each recursive call as follows:
+The basic measures relate at each recursive call as follows:
 (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
             x1 x2
 1) 17:12-47  ?  ?
@@ -39,7 +39,7 @@ no parameters suitable for structural recursion
 
 well-founded recursion cannot be used, 'noNonFixedArguments' does not take any (non-fixed) arguments
 guessLexFailures.lean:27:0-33:31: error: Could not find a decreasing measure.
-The arguments relate at each recursive call as follows:
+The basic measures relate at each recursive call as follows:
 (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
            n m l
 1) 29:6-25 = = =
@@ -47,7 +47,7 @@ The arguments relate at each recursive call as follows:
 3) 31:6-23 < _ _
 Please use `termination_by` to specify a decreasing measure.
 guessLexFailures.lean:37:0-43:31: error: Could not find a decreasing measure.
-The arguments relate at each recursive call as follows:
+The basic measures relate at each recursive call as follows:
 (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
            n m x4
 1) 39:6-27 = =  =
@@ -55,7 +55,7 @@ The arguments relate at each recursive call as follows:
 3) 41:6-25 < _  _
 Please use `termination_by` to specify a decreasing measure.
 guessLexFailures.lean:48:0-54:31: error: Could not find a decreasing measure.
-The arguments relate at each recursive call as follows:
+The basic measures relate at each recursive call as follows:
 (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
            n m l
 1) 50:6-25 = = =
@@ -79,7 +79,7 @@ Skipping arguments of type True, as Mutual.f has no compatible argument.
 
 
 Could not find a decreasing measure.
-The arguments relate at each recursive call as follows:
+The basic measures relate at each recursive call as follows:
 (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
 Call from Mutual.f to Mutual.f at 61:8-33:
  n m l
@@ -128,13 +128,13 @@ Cannot use parameter #2:
 
 
 Could not find a decreasing measure.
-The arguments relate at each recursive call as follows:
+The basic measures relate at each recursive call as follows:
 (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
             n m
 1) 89:19-32 ? ?
 Please use `termination_by` to specify a decreasing measure.
 guessLexFailures.lean:100:0-103:31: error: Could not find a decreasing measure.
-The arguments relate at each recursive call as follows:
+The basic measures relate at each recursive call as follows:
 (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
               n m
 1) 101:83-105 ? ?
@@ -146,7 +146,7 @@ guessLexFailures.lean:113:14-113:31: error: failed to prove termination, possibl
 n✝ m n : Nat
 ⊢ n < n✝
 guessLexFailures.lean:119:0-123:31: error: Could not find a decreasing measure.
-The arguments relate at each recursive call as follows:
+The basic measures relate at each recursive call as follows:
 (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
              n m
 1) 121:31-54 ? ?
diff --git a/tests/lean/guessLexTricky.lean.expected.out b/tests/lean/guessLexTricky.lean.expected.out
index 816a3a696a..debc88d00d 100644
--- a/tests/lean/guessLexTricky.lean.expected.out
+++ b/tests/lean/guessLexTricky.lean.expected.out
@@ -1,6 +1,6 @@
-Inferred termination argument:
+Inferred termination measure:
 termination_by (y, 1, 0)
-Inferred termination argument:
+Inferred termination measure:
 termination_by (y, 0, 1)
-Inferred termination argument:
+Inferred termination measure:
 termination_by (y, 0, 0)
diff --git a/tests/lean/guessLexTricky2.lean.expected.out b/tests/lean/guessLexTricky2.lean.expected.out
index f18a818afe..e59b356d82 100644
--- a/tests/lean/guessLexTricky2.lean.expected.out
+++ b/tests/lean/guessLexTricky2.lean.expected.out
@@ -1,4 +1,4 @@
-Inferred termination argument:
+Inferred termination measure:
 termination_by x1 x2 => (x1, x2, 0)
-Inferred termination argument:
+Inferred termination measure:
 termination_by x1 x2 => (x1, x2, 1)
diff --git a/tests/lean/issue2260.lean.expected.out b/tests/lean/issue2260.lean.expected.out
index fe8245abd9..16d1312800 100644
--- a/tests/lean/issue2260.lean.expected.out
+++ b/tests/lean/issue2260.lean.expected.out
@@ -1,9 +1,9 @@
-issue2260.lean:8:0-8:21: error: The termination argument's type must not depend on the function's varying parameters, but foo's termination argument does:
+issue2260.lean:8:0-8:21: error: The termination measure's type must not depend on the function's varying parameters, but foo's termination measure does:
   {i : Nat} → DNat i → DNat i
 Try using `sizeOf` explicitly
-issue2260.lean:15:0-15:21: error: The termination argument's type must not depend on the function's varying parameters, but bar1's termination argument does:
+issue2260.lean:15:0-15:21: error: The termination measure's type must not depend on the function's varying parameters, but bar1's termination measure does:
   {i : Nat} → DNat i → DNat i
 Try using `sizeOf` explicitly
-issue2260.lean:31:0-31:21: error: The termination argument's type must not depend on the function's varying parameters, but baz2's termination argument does:
+issue2260.lean:31:0-31:21: error: The termination measure's type must not depend on the function's varying parameters, but baz2's termination measure does:
   {i : Nat} → DNat i → DNat i
 Try using `sizeOf` explicitly
diff --git a/tests/lean/mutwftypemismatch.lean.expected.out b/tests/lean/mutwftypemismatch.lean.expected.out
index b922615308..c2961c5451 100644
--- a/tests/lean/mutwftypemismatch.lean.expected.out
+++ b/tests/lean/mutwftypemismatch.lean.expected.out
@@ -1,10 +1,10 @@
-mutwftypemismatch.lean:11:0-11:25: error: The termination arguments of mutually recursive functions must have the same return type, but the termination argument of Ex1.foo has type
+mutwftypemismatch.lean:11:0-11:25: error: The termination measures of mutually recursive functions must have the same return type, but the termination measure of Ex1.foo has type
   Nat
-while the termination argument of Ex1.bar has type
+while the termination measure of Ex1.bar has type
   Prop
 Try using `sizeOf` explicitly
-mutwftypemismatch.lean:26:0-26:44: error: The termination arguments of mutually recursive functions must have the same return type, but the termination argument of Ex2.foo has type
+mutwftypemismatch.lean:26:0-26:44: error: The termination measures of mutually recursive functions must have the same return type, but the termination measure of Ex2.foo has type
   Nat
-while the termination argument of Ex2.bar has type
+while the termination measure of Ex2.bar has type
   Fin fixed
 Try using `sizeOf` explicitly
diff --git a/tests/lean/run/issue4671.lean b/tests/lean/run/issue4671.lean
index e364cb4f23..47dd047082 100644
--- a/tests/lean/run/issue4671.lean
+++ b/tests/lean/run/issue4671.lean
@@ -5,7 +5,7 @@ inductive  A (n : Nat) : Type
   | b : A n → A n
 
 /--
-error: cannot use specified parameter for structural recursion:
+error: cannot use specified measure for structural recursion:
   its type is an inductive datatype
     A n
   and the datatype parameter
@@ -28,7 +28,7 @@ inductive Xn (e : Sigma.{0} (· → Type)) (α : Type) : Nat → Type where
 | mk2 {n} (s : e.1) (p : e.2 s → Xn e α n) : Xn e α n
 
 /--
-error: cannot use specified parameter for structural recursion:
+error: cannot use specified measure for structural recursion:
   its type is an inductive datatype
     Xn e (Xn e α n) m
   and the datatype parameter
diff --git a/tests/lean/run/structuralMutual.lean b/tests/lean/run/structuralMutual.lean
index 24eba94e9d..24a44208d2 100644
--- a/tests/lean/run/structuralMutual.lean
+++ b/tests/lean/run/structuralMutual.lean
@@ -415,7 +415,7 @@ inductive  B (n : Nat) : Type
 end
 
 /--
-error: cannot use specified parameter for structural recursion:
+error: cannot use specified measure for structural recursion:
   its type is an inductive datatype
     A n
   and the datatype parameter
@@ -439,7 +439,7 @@ end
 end Mutual3
 
 /--
-error: cannot use specified parameter for structural recursion:
+error: cannot use specified measure for structural recursion:
   its type FixedIndex.T is an inductive family and indices are not variables
     T 37
 -/
@@ -460,7 +460,7 @@ inductive T (n : Nat) : Nat → Type where
   | n : T n n → T n n
 
 /--
-error: cannot use specified parameter for structural recursion:
+error: cannot use specified measure for structural recursion:
   its type is an inductive datatype
     T n n
   and the datatype parameter
@@ -523,7 +523,7 @@ Too many possible combinations of parameters of type Nattish (or please indicate
 
 
 Could not find a decreasing measure.
-The arguments relate at each recursive call as follows:
+The basic measures relate at each recursive call as follows:
 (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
 Call from ManyCombinations.f to ManyCombinations.g at 557:15-29:
    #1 #2 #3 #4
diff --git a/tests/lean/run/terminationByStructurally.lean b/tests/lean/run/terminationByStructurally.lean
index 2b34bccd65..d7722275c7 100644
--- a/tests/lean/run/terminationByStructurally.lean
+++ b/tests/lean/run/terminationByStructurally.lean
@@ -19,7 +19,7 @@ namespace Errors
 -- A few error conditions
 
 /--
-error: cannot use specified parameter for structural recursion:
+error: cannot use specified measure for structural recursion:
   it is unchanged in the recursive calls
 -/
 #guard_msgs in
@@ -27,7 +27,7 @@ def foo1 (n : Nat) : Nat := foo1 n
 termination_by structural n
 
 /--
-error: cannot use specified parameter for structural recursion:
+error: cannot use specified measure for structural recursion:
   its type Nat.le is an inductive family and indices are not variables
     n.succ.le 100
 -/
@@ -73,7 +73,7 @@ def ackermann2 (n m : Nat) := match n, m with
 termination_by structural m
 
 /--
-error: The termination argument of a structurally recursive function must be one of the parameters 'n', but
+error: The termination measure of a structurally recursive function must be one of the parameters 'n', but
   id n + 1
 isn't one of these.
 -/
diff --git a/tests/lean/terminationFailure.lean.expected.out b/tests/lean/terminationFailure.lean.expected.out
index cc8cf78575..915a4de9ec 100644
--- a/tests/lean/terminationFailure.lean.expected.out
+++ b/tests/lean/terminationFailure.lean.expected.out
@@ -9,7 +9,7 @@ Cannot use parameters #1 of f.g and x of f:
 
 
 Could not find a decreasing measure.
-The arguments relate at each recursive call as follows:
+The basic measures relate at each recursive call as follows:
 (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
 Call from f.g to f at 9:9-12:
   x1
diff --git a/tests/lean/wf1.lean.expected.out b/tests/lean/wf1.lean.expected.out
index 3d1f386297..36d1f2dd68 100644
--- a/tests/lean/wf1.lean.expected.out
+++ b/tests/lean/wf1.lean.expected.out
@@ -11,7 +11,7 @@ Cannot use parameter y:
 
 
 Could not find a decreasing measure.
-The arguments relate at each recursive call as follows:
+The basic measures relate at each recursive call as follows:
 (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
            x y y - x
 1) 3:12-19 ≤ ?     ?