From a24a7772a0a18fa612963252caf4d4a8594bd343 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Tue, 27 Feb 2024 11:59:54 +0100
Subject: [PATCH 1/6] feat: termination_by?
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

the user can now write `termination_by?` to see the termination argument
inferred by GuessLex, and turn it into `termination_by …` using the “Try
this” widget or a code action.
---
 src/Lean/Elab/PreDefinition/WF/GuessLex.lean  |  9 ++++---
 .../PreDefinition/WF/TerminationHint.lean     | 27 +++++++++++--------
 src/Lean/Parser/Term.lean                     | 14 ++++++----
 stage0/src/stdlib_flags.h                     |  2 +-
 .../interactive/terminationBySuggestion.lean  |  7 +++++
 .../terminationBySuggestion.lean.expected.out | 12 +++++++++
 6 files changed, 51 insertions(+), 20 deletions(-)
 create mode 100644 tests/lean/interactive/terminationBySuggestion.lean
 create mode 100644 tests/lean/interactive/terminationBySuggestion.lean.expected.out

diff --git a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean
index 523ba0db00bd..ca674fcfefb2 100644
--- a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean
+++ b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean
@@ -8,6 +8,7 @@ import Lean.Util.HasConstCache
 import Lean.Meta.Match.MatcherApp.Transform
 import Lean.Meta.Tactic.Cleanup
 import Lean.Meta.Tactic.Refl
+import Lean.Meta.Tactic.TryThis
 import Lean.Elab.Quotation
 import Lean.Elab.RecAppSyntax
 import Lean.Elab.PreDefinition.Basic
@@ -709,10 +710,12 @@ def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition)
   | .some solution => do
     let wf ← buildTermWF originalVarNamess varNamess solution
 
-    if showInferredTerminationBy.get (← getOptions) then
-      let wf' := trimTermWF extraParamss wf
-      for preDef in preDefs, term in wf' do
+    let wf' := trimTermWF extraParamss wf
+    for preDef in preDefs, term in wf' do
+      if showInferredTerminationBy.get (← getOptions) then
         logInfoAt preDef.ref m!"Inferred termination argument: {← term.unexpand}"
+      if let some ref := preDef.termination.termination_by?? then
+        Tactic.TryThis.addSuggestion ref (← term.unexpand)
 
     return wf
   | .none =>
diff --git a/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean b/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean
index 22d34c6687be..2d130209f8f4 100644
--- a/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean
+++ b/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean
@@ -27,7 +27,7 @@ structure TerminationBy where
   deriving Inhabited
 
 open Parser.Termination in
-def TerminationBy.unexpand (wf : TerminationBy) : MetaM Syntax := do
+def TerminationBy.unexpand (wf : TerminationBy) : MetaM (TSyntax ``terminationBy) := do
   -- TODO: Why can I not just use $wf.vars in the quotation below?
   let vars : TSyntaxArray `ident := wf.vars.map (⟨·.raw⟩)
   if vars.isEmpty then
@@ -50,6 +50,7 @@ is what `Term.runTactic` expects.
  -/
 structure TerminationHints where
   ref : Syntax
+  termination_by?? : Option Syntax
   termination_by? : Option TerminationBy
   decreasing_by?  : Option DecreasingBy
   /-- Here we record the number of parameters past the `:`. It is set by
@@ -63,7 +64,7 @@ structure TerminationHints where
   extraParams : Nat
   deriving Inhabited
 
-def TerminationHints.none : TerminationHints := ⟨.missing, .none, .none, 0⟩
+def TerminationHints.none : TerminationHints := ⟨.missing, .none, .none, .none, 0⟩
 
 /-- Logs warnings when the `TerminationHints` are present.  -/
 def TerminationHints.ensureNone (hints : TerminationHints) (reason : String): CoreM Unit := do
@@ -111,19 +112,23 @@ def elabTerminationHints {m} [Monad m] [MonadError m] (stx : TSyntax ``suffix) :
   if let .missing := stx.raw then
     return { TerminationHints.none with ref := stx }
   match stx with
-  | `(suffix| $[$t?:terminationBy]? $[$d?:decreasingBy]? ) => do
-    let termination_by? ← t?.mapM fun t => match t with
-      | `(terminationBy|termination_by $vars* => $body) =>
-        if vars.isEmpty then
-          throwErrorAt t "no extra parameters bounds, please omit the `=>`"
-        else
-          pure {ref := t, vars, body}
-      | `(terminationBy|termination_by $body:term) => pure {ref := t, vars := #[], body}
+  | `(suffix| $[$t?]? $[$d?:decreasingBy]? ) => do
+    let termination_by?? : Option Syntax ← if let some t := t? then match t with
+      | `(terminationBy?|termination_by?) => pure (some t)
+      | _ => pure none
+      else pure none
+    let termination_by? : Option TerminationBy ← if let some t := t? then match t with
+      | `(terminationBy|termination_by => $_body) =>
+        throwErrorAt t "no extra parameters bounds, please omit the `=>`"
+      | `(terminationBy|termination_by $vars* => $body) => pure (some {ref := t, vars, body})
+      | `(terminationBy|termination_by $body:term) => pure (some {ref := t, vars := #[], body})
+      | `(terminationBy?|termination_by?) => pure none
       | _ => throwErrorAt t "unexpected `termination_by` syntax"
+      else pure none
     let decreasing_by? ← d?.mapM fun d => match d with
       | `(decreasingBy|decreasing_by $tactic) => pure {ref := d, tactic}
       | _ => throwErrorAt d "unexpected `decreasing_by` syntax"
-    return { ref := stx, termination_by?, decreasing_by?, extraParams := 0 }
+    return { ref := stx, termination_by??, termination_by?, decreasing_by?, extraParams := 0 }
   | _ => throwErrorAt stx s!"Unexpected Termination.suffix syntax: {stx} of kind {stx.raw.getKind}"
 
 end Lean.Elab.WF
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index ba66b5669a9a..aff824e5a9a0 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -118,13 +118,17 @@ def example (a : Nat) : Nat → Nat → Nat :=
 termination_by b c => a - b
 ```
 
-If omitted, a termination argument will be inferred.
+If omitted, a termination argument will be inferred. If written as `termination_by?`,
+the inferrred termination argument will be suggested.
 -/
 def terminationBy := leading_parser
-  ppDedent ppLine >>
   "termination_by " >>
-  optional (atomic (many (ppSpace >> (ident <|> "_")) >> " => ")) >>
-  termParser
+    optional (atomic (many (ppSpace >> (ident <|> "_")) >> " => ")) >>
+    termParser
+
+@[inherit_doc terminationBy]
+def terminationBy? := leading_parser
+  "termination_by?"
 
 /--
 Manually prove that the termination argument (as specified with `termination_by` or inferred)
@@ -139,7 +143,7 @@ def decreasingBy := leading_parser
 Termination hints are `termination_by` and `decreasing_by`, in that order.
 -/
 def suffix := leading_parser
-  optional terminationBy >> optional decreasingBy
+  optional (ppDedent ppLine >> (terminationBy? <|> terminationBy)) >> optional decreasingBy
 
 end Termination
 
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index 0699845ba452..658ab0874e68 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -8,7 +8,7 @@ options get_default_options() {
     // switch to `true` for ABI-breaking changes affecting meta code
     opts = opts.update({"interpreter", "prefer_native"}, false);
     // switch to `true` for changing built-in parsers used in quotations
-    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false);
+    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, true);
     // toggling `parseQuotWithCurrentStage` may also require toggling the following option if macros/syntax
     // with custom precheck hooks were affected
     opts = opts.update({"quotPrecheck"}, true);
diff --git a/tests/lean/interactive/terminationBySuggestion.lean b/tests/lean/interactive/terminationBySuggestion.lean
new file mode 100644
index 000000000000..928c0cc081fb
--- /dev/null
+++ b/tests/lean/interactive/terminationBySuggestion.lean
@@ -0,0 +1,7 @@
+
+def ackermann (n m : Nat) := match n, m with
+  | 0, m => m + 1
+  | .succ n, 0 => ackermann n 1
+  | .succ n, .succ m => ackermann n (ackermann (n + 1) m)
+termination_by?
+   --^ codeAction
diff --git a/tests/lean/interactive/terminationBySuggestion.lean.expected.out b/tests/lean/interactive/terminationBySuggestion.lean.expected.out
new file mode 100644
index 000000000000..a1c73f09d83f
--- /dev/null
+++ b/tests/lean/interactive/terminationBySuggestion.lean.expected.out
@@ -0,0 +1,12 @@
+{"title": "Try this: termination_by (sizeOf n, sizeOf m)",
+ "kind": "quickfix",
+ "isPreferred": true,
+ "edit":
+ {"documentChanges":
+  [{"textDocument":
+    {"version": 1, "uri": "file:///terminationBySuggestion.lean"},
+    "edits":
+    [{"range":
+      {"start": {"line": 5, "character": 0},
+       "end": {"line": 5, "character": 15}},
+      "newText": "termination_by (sizeOf n, sizeOf m)"}]}]}}

From 3f0acaafaab4626aaf60e3d64e27287769c7a6a9 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Tue, 27 Feb 2024 14:36:40 +0100
Subject: [PATCH 2/6] Fix test output

---
 src/Lean/Elab/PreDefinition/WF/GuessLex.lean |  2 +-
 tests/lean/guessLex.lean.expected.out        | 40 ++++++++++----------
 tests/lean/guessLexTricky.lean.expected.out  |  6 +--
 tests/lean/guessLexTricky2.lean.expected.out |  4 +-
 4 files changed, 26 insertions(+), 26 deletions(-)

diff --git a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean
index ca674fcfefb2..e17e034d9b89 100644
--- a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean
+++ b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean
@@ -713,7 +713,7 @@ def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition)
     let wf' := trimTermWF extraParamss wf
     for preDef in preDefs, term in wf' do
       if showInferredTerminationBy.get (← getOptions) then
-        logInfoAt preDef.ref m!"Inferred termination argument: {← term.unexpand}"
+        logInfoAt preDef.ref m!"Inferred termination argument:\n{← term.unexpand}"
       if let some ref := preDef.termination.termination_by?? then
         Tactic.TryThis.addSuggestion ref (← term.unexpand)
 
diff --git a/tests/lean/guessLex.lean.expected.out b/tests/lean/guessLex.lean.expected.out
index b3939d68e4f9..7101d313ae0c 100644
--- a/tests/lean/guessLex.lean.expected.out
+++ b/tests/lean/guessLex.lean.expected.out
@@ -1,41 +1,41 @@
-Inferred termination argument: 
+Inferred termination argument:
 termination_by (sizeOf n, sizeOf m)
-Inferred termination argument: 
+Inferred termination argument:
 termination_by (sizeOf m, sizeOf n)
-Inferred termination argument: 
+Inferred termination argument:
 termination_by (sizeOf n, sizeOf m)
-Inferred termination argument: 
+Inferred termination argument:
 termination_by x1 x2 => (sizeOf x2, sizeOf x1)
-Inferred termination argument: 
+Inferred termination argument:
 termination_by x1 => sizeOf x1
-Inferred termination argument: 
+Inferred termination argument:
 termination_by x1 => sizeOf x1
-Inferred termination argument: 
+Inferred termination argument:
 termination_by x1 => sizeOf x1
-Inferred termination argument: 
+Inferred termination argument:
 termination_by x1 => sizeOf x1
-Inferred termination argument: 
+Inferred termination argument:
 termination_by x1 => (sizeOf x1, 0)
-Inferred termination argument: 
+Inferred termination argument:
 termination_by (sizeOf n, 1)
-Inferred termination argument: 
+Inferred termination argument:
 termination_by (sizeOf m, sizeOf n)
-Inferred termination argument: 
+Inferred termination argument:
 termination_by x1 x2 x3 x4 x5 x6 x7 x8 =>
   (sizeOf x8, sizeOf x7, sizeOf x6, sizeOf x5, sizeOf x4, sizeOf x3, sizeOf x2, sizeOf x1)
-Inferred termination argument: 
+Inferred termination argument:
 termination_by x1 x2 => (sizeOf x1, sizeOf x2)
-Inferred termination argument: 
+Inferred termination argument:
 termination_by (sizeOf a, 1)
-Inferred termination argument: 
+Inferred termination argument:
 termination_by (sizeOf a, 0)
-Inferred termination argument: 
+Inferred termination argument:
 termination_by x2' => sizeOf x2'
-Inferred termination argument: 
+Inferred termination argument:
 termination_by x2 => sizeOf x2
-Inferred termination argument: 
+Inferred termination argument:
 termination_by x2 => SizeOf.sizeOf x2
-Inferred termination argument: 
+Inferred termination argument:
 termination_by x1 x2 => SizeOf.sizeOf x1
-Inferred termination argument: 
+Inferred termination argument:
 termination_by x2 => SizeOf.sizeOf x2
diff --git a/tests/lean/guessLexTricky.lean.expected.out b/tests/lean/guessLexTricky.lean.expected.out
index 389959b3e5b0..6e98a304c024 100644
--- a/tests/lean/guessLexTricky.lean.expected.out
+++ b/tests/lean/guessLexTricky.lean.expected.out
@@ -1,6 +1,6 @@
-Inferred termination argument: 
+Inferred termination argument:
 termination_by (sizeOf y, 1, 0)
-Inferred termination argument: 
+Inferred termination argument:
 termination_by (sizeOf y, 0, 1)
-Inferred termination argument: 
+Inferred termination argument:
 termination_by (sizeOf y, 0, 0)
diff --git a/tests/lean/guessLexTricky2.lean.expected.out b/tests/lean/guessLexTricky2.lean.expected.out
index 758c630cb03b..24db6dc1bfbe 100644
--- a/tests/lean/guessLexTricky2.lean.expected.out
+++ b/tests/lean/guessLexTricky2.lean.expected.out
@@ -1,4 +1,4 @@
-Inferred termination argument: 
+Inferred termination argument:
 termination_by x1 x2 x3 => (sizeOf x1, sizeOf x2, 0)
-Inferred termination argument: 
+Inferred termination argument:
 termination_by x1 x2 x3 => (sizeOf x1, sizeOf x2, 1)

From a5a6c50ed87314581bafecb2e9e089674f8a0a51 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Tue, 27 Feb 2024 23:20:38 +0100
Subject: [PATCH 3/6] Reduce diff

---
 src/Lean/Parser/Term.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index aff824e5a9a0..3eadf04ae3ab 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -123,8 +123,8 @@ the inferrred termination argument will be suggested.
 -/
 def terminationBy := leading_parser
   "termination_by " >>
-    optional (atomic (many (ppSpace >> (ident <|> "_")) >> " => ")) >>
-    termParser
+  optional (atomic (many (ppSpace >> (ident <|> "_")) >> " => ")) >>
+  termParser
 
 @[inherit_doc terminationBy]
 def terminationBy? := leading_parser

From 9491876d4cf67327feac764ca1db8a959945553d Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Wed, 28 Feb 2024 10:02:41 +0100
Subject: [PATCH 4/6] Avoid new keyword in code

---
 src/Lean/Elab/PreDefinition/Main.lean         |  3 +-
 src/Lean/Elab/PreDefinition/WF/GuessLex.lean  |  2 +-
 src/Lean/Elab/PreDefinition/WF/Main.lean      |  4 +--
 .../PreDefinition/WF/TerminationHint.lean     | 32 ++++++++++++-------
 4 files changed, 24 insertions(+), 17 deletions(-)

diff --git a/src/Lean/Elab/PreDefinition/Main.lean b/src/Lean/Elab/PreDefinition/Main.lean
index c72586a35706..037b0ca60008 100644
--- a/src/Lean/Elab/PreDefinition/Main.lean
+++ b/src/Lean/Elab/PreDefinition/Main.lean
@@ -121,8 +121,7 @@ def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLC
       preDefs.forM (·.termination.ensureNone "partial")
     else
       try
-        let hasHints := preDefs.any  fun preDef =>
-          preDef.termination.decreasing_by?.isSome || preDef.termination.termination_by?.isSome
+        let hasHints := preDefs.any fun preDef => preDef.termination.isNotNone
         if hasHints then
           wfRecursion preDefs
         else
diff --git a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean
index e17e034d9b89..5be7c4984775 100644
--- a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean
+++ b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean
@@ -714,7 +714,7 @@ def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition)
     for preDef in preDefs, term in wf' do
       if showInferredTerminationBy.get (← getOptions) then
         logInfoAt preDef.ref m!"Inferred termination argument:\n{← term.unexpand}"
-      if let some ref := preDef.termination.termination_by?? then
+      if let some ref := preDef.termination.terminationBy?? then
         Tactic.TryThis.addSuggestion ref (← term.unexpand)
 
     return wf
diff --git a/src/Lean/Elab/PreDefinition/WF/Main.lean b/src/Lean/Elab/PreDefinition/WF/Main.lean
index eccce4360c6e..45ed72ba3f26 100644
--- a/src/Lean/Elab/PreDefinition/WF/Main.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Main.lean
@@ -94,12 +94,12 @@ def wfRecursion (preDefs : Array PreDefinition) : TermElabM Unit := do
     return (← packMutual fixedPrefixSize preDefs unaryPreDefs, fixedPrefixSize)
 
   let wf ← do
-    let (preDefsWith, preDefsWithout) := preDefs.partition (·.termination.termination_by?.isSome)
+    let (preDefsWith, preDefsWithout) := preDefs.partition (·.termination.terminationBy?.isSome)
     if preDefsWith.isEmpty then
       -- No termination_by anywhere, so guess one
       guessLex preDefs unaryPreDef fixedPrefixSize
     else if preDefsWithout.isEmpty then
-      pure <| preDefsWith.map (·.termination.termination_by?.get!)
+      pure <| preDefsWith.map (·.termination.terminationBy?.get!)
     else
       -- Some have, some do not, so report errors
       preDefsWithout.forM fun preDef => do
diff --git a/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean b/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean
index 2d130209f8f4..aced55dab80f 100644
--- a/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean
+++ b/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean
@@ -50,9 +50,9 @@ is what `Term.runTactic` expects.
  -/
 structure TerminationHints where
   ref : Syntax
-  termination_by?? : Option Syntax
-  termination_by? : Option TerminationBy
-  decreasing_by?  : Option DecreasingBy
+  terminationBy?? : Option Syntax
+  terminationBy? : Option TerminationBy
+  decreasingBy?  : Option DecreasingBy
   /-- Here we record the number of parameters past the `:`. It is set by
   `TerminationHints.rememberExtraParams` and used as folows:
 
@@ -68,15 +68,23 @@ def TerminationHints.none : TerminationHints := ⟨.missing, .none, .none, .none
 
 /-- Logs warnings when the `TerminationHints` are present.  -/
 def TerminationHints.ensureNone (hints : TerminationHints) (reason : String): CoreM Unit := do
-  match hints.termination_by?, hints.decreasing_by? with
-  | .none, .none => pure ()
-  | .none, .some dec_by =>
+  match hints.terminationBy??, hints.terminationBy?, hints.decreasingBy? with
+  | .none, .none, .none => pure ()
+  | .none, .none, .some dec_by =>
     logErrorAt dec_by.ref m!"unused `decreasing_by`, function is {reason}"
-  | .some term_by, .none =>
+  | .some term_by?, .none, .none =>
+    logErrorAt term_by? m!"unused `termination_by?`, function is {reason}"
+  | .none, .some term_by, .none =>
     logErrorAt term_by.ref m!"unused `termination_by`, function is {reason}"
-  | .some _, .some _ =>
+  | _, _, _ =>
     logErrorAt hints.ref m!"unused termination hints, function is {reason}"
 
+/-- True if any form of termination hint is present. -/
+def TerminationHints.isNotNone (hints : TerminationHints) : Bool :=
+  hints.terminationBy??.isSome ||
+  hints.terminationBy?.isSome ||
+  hints.decreasingBy?.isSome
+
 /--
 Remembers `extraParams` for later use. Needs to happen early enough where we still know
 how many parameters came from the function header (`headerParams`).
@@ -113,11 +121,11 @@ def elabTerminationHints {m} [Monad m] [MonadError m] (stx : TSyntax ``suffix) :
     return { TerminationHints.none with ref := stx }
   match stx with
   | `(suffix| $[$t?]? $[$d?:decreasingBy]? ) => do
-    let termination_by?? : Option Syntax ← if let some t := t? then match t with
+    let terminationBy?? : Option Syntax ← if let some t := t? then match t with
       | `(terminationBy?|termination_by?) => pure (some t)
       | _ => pure none
       else pure none
-    let termination_by? : Option TerminationBy ← if let some t := t? then match t with
+    let terminationBy? : Option TerminationBy ← if let some t := t? then match t with
       | `(terminationBy|termination_by => $_body) =>
         throwErrorAt t "no extra parameters bounds, please omit the `=>`"
       | `(terminationBy|termination_by $vars* => $body) => pure (some {ref := t, vars, body})
@@ -125,10 +133,10 @@ def elabTerminationHints {m} [Monad m] [MonadError m] (stx : TSyntax ``suffix) :
       | `(terminationBy?|termination_by?) => pure none
       | _ => throwErrorAt t "unexpected `termination_by` syntax"
       else pure none
-    let decreasing_by? ← d?.mapM fun d => match d with
+    let decreasingBy? ← d?.mapM fun d => match d with
       | `(decreasingBy|decreasing_by $tactic) => pure {ref := d, tactic}
       | _ => throwErrorAt d "unexpected `decreasing_by` syntax"
-    return { ref := stx, termination_by??, termination_by?, decreasing_by?, extraParams := 0 }
+    return { ref := stx, terminationBy??, terminationBy?, decreasingBy?, extraParams := 0 }
   | _ => throwErrorAt stx s!"Unexpected Termination.suffix syntax: {stx} of kind {stx.raw.getKind}"
 
 end Lean.Elab.WF

From fd0187d46d88f9c71232c9981d321ee3ac7d50f1 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Wed, 28 Feb 2024 10:50:26 +0100
Subject: [PATCH 5/6] Update GuessLex.lean

---
 src/Lean/Elab/PreDefinition/WF/GuessLex.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean
index 5be7c4984775..419f6b8ed0af 100644
--- a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean
+++ b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean
@@ -703,7 +703,7 @@ def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition)
   -- Collect all recursive calls and extract their context
   let recCalls ← collectRecCalls unaryPreDef fixedPrefixSize arities
   let recCalls := filterSubsumed recCalls
-  let rcs ← recCalls.mapM (RecCallCache.mk (preDefs.map (·.termination.decreasing_by?)) ·)
+  let rcs ← recCalls.mapM (RecCallCache.mk (preDefs.map (·.termination.decreasingBy?)) ·)
   let callMatrix := rcs.map (inspectCall ·)
 
   match ← liftMetaM <| solve measures callMatrix with

From 5eb120d1d137964a22caf40ba9aec6417c0404fc Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Wed, 28 Feb 2024 11:16:17 +0100
Subject: [PATCH 6/6] Update Main.lean

---
 src/Lean/Elab/PreDefinition/WF/Main.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Elab/PreDefinition/WF/Main.lean b/src/Lean/Elab/PreDefinition/WF/Main.lean
index 45ed72ba3f26..b20687ca7af8 100644
--- a/src/Lean/Elab/PreDefinition/WF/Main.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Main.lean
@@ -114,7 +114,7 @@ def wfRecursion (preDefs : Array PreDefinition) : TermElabM Unit := do
       trace[Elab.definition.wf] "wfRel: {wfRel}"
       let (value, envNew) ← withoutModifyingEnv' do
         addAsAxiom unaryPreDef
-        let value ← mkFix unaryPreDef prefixArgs wfRel (preDefs.map (·.termination.decreasing_by?))
+        let value ← mkFix unaryPreDef prefixArgs wfRel (preDefs.map (·.termination.decreasingBy?))
         eraseRecAppSyntaxExpr value
       /- `mkFix` invokes `decreasing_tactic` which may add auxiliary theorems to the environment. -/
       let value ← unfoldDeclsFrom envNew value