add test

doc/dev/ffi.md

@@ -121,4 +121,4 @@ Thus to e.g. run `#eval` on such a declaration, you need to
 Note that it is not sufficient to load the foreign library containing the external symbol because the interpreter depends on code that is emitted for each `@[extern]` declaration.
 Thus it is not possible to interpret an `@[extern]` declaration in the same file.
 
-See [`tests/compiler/foreign`](https://github.com/leanprover/lean4/tree/master/tests/compiler/foreign/) for an example.
+See `tests/compiler/foreign` for an example.

doc/dev/testing.md

@@ -41,17 +41,17 @@ information is displayed. This option will show all test output.
 
 All these tests are included by [src/shell/CMakeLists.txt](https://github.com/leanprover/lean4/blob/master/src/shell/CMakeLists.txt):
 
-- [`tests/lean`](https://github.com/leanprover/lean4/tree/master/tests/lean/): contains tests that come equipped with a
-  .lean.expected.out file. The driver script [`test_single.sh`](https://github.com/leanprover/lean4/tree/master/tests/lean/test_single.sh) runs
+- `tests/lean`: contains tests that come equipped with a
+  .lean.expected.out file. The driver script `test_single.sh` runs
   each test and checks the actual output (*.produced.out) with the
   checked in expected output.
 
-- [`tests/lean/run`](https://github.com/leanprover/lean4/tree/master/tests/lean/run/): contains tests that are run through the lean
+- `tests/lean/run`: contains tests that are run through the lean
   command line one file at a time. These tests only look for error
   codes and do not check the expected output even though output is
   produced, it is ignored.
 
-- [`tests/lean/interactive`](https://github.com/leanprover/lean4/tree/master/tests/lean/interactive/): are designed to test server requests at a
+- `tests/lean/interactive`: are designed to test server requests at a
   given position in the input file. Each .lean file contains comments
   that indicate how to simulate a client request at that position.
   using a `--^` point to the line position. Example:
@@ -61,7 +61,7 @@ All these tests are included by [src/shell/CMakeLists.txt](https://github.com/le
     Bla.
       --^ textDocument/completion
     ```
-    In this example, the test driver [`test_single.sh`](https://github.com/leanprover/lean4/tree/master/tests/lean/interactive/test_single.sh) will simulate an
+    In this example, the test driver `test_single.sh` will simulate an
     auto-completion request at `Bla.`. The expected output is stored in
     a .lean.expected.out in the json format that is part of the
     [Language Server
@@ -78,21 +78,21 @@ All these tests are included by [src/shell/CMakeLists.txt](https://github.com/le
     --^ collectDiagnostics
     ```
 
-- [`tests/lean/server`](https://github.com/leanprover/lean4/tree/master/tests/lean/server/): Tests more of the Lean `--server` protocol.
+- `tests/lean/server`: Tests more of the Lean `--server` protocol.
   There are just a few of them, and it uses .log files containing
   JSON.
 
-- [`tests/compiler`](https://github.com/leanprover/lean4/tree/master/tests/compiler/): contains tests that will run the Lean compiler and
+- `tests/compiler`: contains tests that will run the Lean compiler and
   build an executable that is executed and the output is compared to
   the .lean.expected.out file. This test also contains a subfolder
-  [`foreign`](https://github.com/leanprover/lean4/tree/master/tests/compiler/foreign/) which shows how to extend Lean using C++.
+  `foreign` which shows how to extend Lean using C++.
 
-- [`tests/lean/trust0`](https://github.com/leanprover/lean4/tree/master/tests/lean/trust0): tests that run Lean in a mode that Lean doesn't
+- `tests/lean/trust0`: tests that run Lean in a mode that Lean doesn't
   even trust the .olean files (i.e., trust 0).
 
-- [`tests/bench`](https://github.com/leanprover/lean4/tree/master/tests/bench/): contains performance tests.
+- `tests/bench`: contains performance tests.
 
-- [`tests/plugin`](https://github.com/leanprover/lean4/tree/master/tests/plugin/): tests that compiled Lean code can be loaded into
+- `tests/plugin`: tests that compiled Lean code can be loaded into
   `lean` via the `--plugin` command line option.
 
 ## Writing Good Tests
@@ -103,7 +103,7 @@ Every test file should contain:
   and, if not 100% clear, why that is the desirable behavior
 
 At the time of writing, most tests do not follow these new guidelines yet.
-For an example of a conforming test, see [`tests/lean/1971.lean`](https://github.com/leanprover/lean4/tree/master/tests/lean/1971.lean).
+For an example of a conforming test, see `tests/lean/1971.lean`.
 
 ## Fixing Tests
 
@@ -119,7 +119,7 @@ First, we must install [meld](http://meldmerge.org/). On Ubuntu, we can do it by
 sudo apt-get install meld
 ```
 
-Now, suppose `bad_class.lean` test is broken. We can see the problem by going to [`tests/lean`](https://github.com/leanprover/lean4/tree/master/tests/lean) directory and
+Now, suppose `bad_class.lean` test is broken. We can see the problem by going to `tests/lean` directory and
 executing
 
 ```

src/Init/Data/Format/Basic.lean

@@ -300,18 +300,11 @@ instance : MonadPrettyFormat (StateM State) where
   startTag _         := return ()
   endTags _          := return ()
 
-/--
-Renders a `Format` to a string.
-* `width`: the total width
-* `indent`: the initial indentation to use for wrapped lines
-  (subsequent wrapping may increase the indentation)
-* `column`: begin the first line wrap `column` characters earlier than usual
-  (this is useful when the output String will be printed starting at `column`)
--/
+/-- Pretty-print a `Format` object as a string with expected width `w`. -/
 @[export lean_format_pretty]
-def pretty (f : Format) (width : Nat := defWidth) (indent : Nat := 0) (column := 0) : String :=
-  let act : StateM State Unit := prettyM f width indent
-  State.out <| act (State.mk "" column) |>.snd
+def pretty (f : Format) (w : Nat := defWidth) : String :=
+  let act: StateM State Unit := prettyM f w
+  act {} |>.snd.out
 
 end Format
 

src/Init/Meta.lean

@@ -563,17 +563,8 @@ def SepArray.ofElemsUsingRef [Monad m] [MonadRef m] {sep} (elems : Array Syntax)
 instance : Coe (Array Syntax) (SepArray sep) where
   coe := SepArray.ofElems
 
-/--
-Constructs a typed separated array from elements.
-The given array does not include the separators.
-
-Like `Syntax.SepArray.ofElems` but for typed syntax.
--/
-def TSepArray.ofElems {sep} (elems : Array (TSyntax k)) : TSepArray k sep :=
-  .mk (SepArray.ofElems (sep := sep) (TSyntaxArray.raw elems)).1
-
 instance : Coe (TSyntaxArray k) (TSepArray k sep) where
-  coe := TSepArray.ofElems
+  coe a := ⟨mkSepArray a.raw (mkAtom sep)⟩
 
 /-- Create syntax representing a Lean term application, but avoid degenerate empty applications. -/
 def mkApp (fn : Term) : (args : TSyntaxArray `term) → Term

src/Lean/Data/Json.lean

@@ -8,4 +8,3 @@ import Lean.Data.Json.Stream
 import Lean.Data.Json.Printer
 import Lean.Data.Json.Parser
 import Lean.Data.Json.FromToJson
-import Lean.Data.Json.Elab

src/Lean/Data/Json/Elab.lean

@@ -1,79 +0,0 @@
-/-
- Copyright (c) 2022 E.W.Ayers. All rights reserved.
- Released under Apache 2.0 license as described in the file LICENSE.
- Authors: E.W.Ayers, Wojciech Nawrocki
--/
-import Lean.Data.Json.FromToJson
-import Lean.Syntax
-
-/-!
-# JSON-like syntax for Lean.
-
-Now you can write
-
-```lean
-open Lean.Json
-
-#eval json% {
-  hello : "world",
-  cheese : ["edam", "cheddar", {kind : "spicy", rank : 100.2}],
-  lemonCount : 100e30,
-  isCool : true,
-  isBug : null,
-  lookACalc: $(23 + 54 * 2)
-}
-```
--/
-
-namespace Lean.Json
-
-/-- Json syntactic category -/
-declare_syntax_cat json (behavior := symbol)
-/-- Json null value syntax. -/
-syntax "null" : json
-/-- Json true value syntax. -/
-syntax "true" : json
-/-- Json false value syntax. -/
-syntax "false" : json
-/-- Json string syntax. -/
-syntax str : json
-/-- Json number negation syntax for ordinary numbers. -/
-syntax "-"? num : json
-/-- Json number negation syntax for scientific numbers. -/
-syntax "-"? scientific : json
-/-- Json array syntax. -/
-syntax "[" json,* "]" : json
-/-- Json identifier syntax. -/
-syntax jsonIdent := ident <|> str
-/-- Json key/value syntax. -/
-syntax jsonField := jsonIdent ": " json
-/-- Json object syntax. -/
-syntax "{" jsonField,* "}" : json
-/-- Allows to use Json syntax in a Lean file. -/
-syntax "json% " json : term
-
-
-macro_rules
-  | `(json% null)           => `(Lean.Json.null)
-  | `(json% true)           => `(Lean.Json.bool Bool.true)
-  | `(json% false)          => `(Lean.Json.bool Bool.false)
-  | `(json% $n:str)         => `(Lean.Json.str $n)
-  | `(json% $n:num)         => `(Lean.Json.num $n)
-  | `(json% $n:scientific)  => `(Lean.Json.num $n)
-  | `(json% -$n:num)        => `(Lean.Json.num (-$n))
-  | `(json% -$n:scientific) => `(Lean.Json.num (-$n))
-  | `(json% [$[$xs],*])     => `(Lean.Json.arr #[$[json% $xs],*])
-  | `(json% {$[$ks:jsonIdent : $vs:json],*}) => do
-    let ks : Array (TSyntax `term) ← ks.mapM fun
-      | `(jsonIdent| $k:ident) => pure (k.getId |> toString |> quote)
-      | `(jsonIdent| $k:str)   => pure k
-      | _                     => Macro.throwUnsupported
-    `(Lean.Json.mkObj [$[($ks, json% $vs)],*])
-  | `(json% $stx)           =>
-    if stx.raw.isAntiquot then
-      let stx := ⟨stx.raw.getAntiquotTerm⟩
-      `(Lean.toJson $stx)
-    else
-      Macro.throwUnsupported
-
-end Lean.Json

src/Lean/Data/Name.lean

@@ -96,12 +96,6 @@ def quickCmp (n₁ n₂ : Name) : Ordering :=
 def quickLt (n₁ n₂ : Name) : Bool :=
   quickCmp n₁ n₂ == Ordering.lt
 
-/-- Returns true if the name has any numeric components. -/
-def hasNum : Name → Bool
-  | .anonymous => false
-  | .str p _ => p.hasNum
-  | .num _ _ => true
-
 /-- The frontend does not allow user declarations to start with `_` in any of its parts.
    We use name parts starting with `_` internally to create auxiliary names (e.g., `_private`). -/
 def isInternal : Name → Bool
@@ -109,17 +103,6 @@ def isInternal : Name → Bool
   | num p _ => isInternal p
   | _       => false
 
-/--
-The frontend does not allow user declarations to start with `_` in any of its parts.
-We use name parts starting with `_` internally to create auxiliary names (e.g., `_private`).
-
-This function checks if any component of the name starts with `_`, or is numeric.
--/
-def isInternalOrNum : Name → Bool
-  | .str p s => s.get 0 == '_' || isInternalOrNum p
-  | .num _ _ => true
-  | _       => false
-
 /--
 Checks whether the name is an implementation-detail hypothesis name.
 

src/Lean/Elab/LetRec.lean

@@ -97,7 +97,7 @@ private def registerLetRecsToLift (views : Array LetRecDeclView) (fvars : Array
 
   let toLift ← views.mapIdxM fun i view => do
     let value := values[i]!
-    let termination := view.termination.rememberExtraParams view.binderIds.size value
+    let termination ← view.termination.checkVars view.binderIds.size value
     pure {
       ref            := view.ref
       fvarId         := fvars[i]!.fvarId!

src/Lean/Elab/MutualDef.lean

@@ -642,7 +642,7 @@ def pushMain (preDefs : Array PreDefinition) (sectionVars : Array Expr) (mainHea
   mainHeaders.size.foldM (init := preDefs) fun i preDefs => do
     let header := mainHeaders[i]!
     let termination ← declValToTerminationHint header.valueStx
-    let termination := termination.rememberExtraParams header.numParams mainVals[i]!
+    let termination ← termination.checkVars header.numParams mainVals[i]!
     let value ← mkLambdaFVars sectionVars mainVals[i]!
     let type ← mkForallFVars sectionVars header.type
     return preDefs.push {

src/Lean/Elab/PreDefinition/WF/Eqns.lean

@@ -44,8 +44,7 @@ private def rwFixEq (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
 def simpMatchWF? (mvarId : MVarId) : MetaM (Option MVarId) :=
   mvarId.withContext do
     let target ← instantiateMVars (← mvarId.getType)
-    let discharge? ← mvarId.withContext do SplitIf.mkDischarge?
-    let (targetNew, _) ← Simp.main target (← Split.getSimpMatchContext) (methods := { pre, discharge? })
+    let (targetNew, _) ← Simp.main target (← Split.getSimpMatchContext) (methods := { pre, discharge? := SplitIf.discharge? })
     let mvarIdNew ← applySimpResultToTarget mvarId target targetNew
     if mvarId != mvarIdNew then return some mvarIdNew else return none
 where

src/Lean/Elab/PreDefinition/WF/GuessLex.lean

@@ -575,7 +575,7 @@ def buildTermWF (originalVarNamess : Array (Array Name)) (varNamess : Array (Arr
           `($sizeOfIdent $v)
       | .func funIdx' => if funIdx' == funIdx then `(1) else `(0)
     let body ← mkTupleSyntax measureStxs
-    return { ref := .missing, vars := idents, body, synthetic := true }
+    return { ref := .missing, vars := idents, body }
 
 /--
 The TerminationWF produced by GuessLex may mention more variables than allowed in the surface
@@ -585,9 +585,8 @@ The latter works fine in many cases, and is still useful to the user in the tric
 we do that.
 -/
 def trimTermWF (extraParams : Array Nat) (elems : TerminationWF) : TerminationWF :=
-  elems.mapIdx fun funIdx elem => { elem with
-    vars := elem.vars[elem.vars.size - extraParams[funIdx]! : elem.vars.size]
-    synthetic := false }
+  elems.mapIdx fun funIdx elem =>
+    { elem with vars := elem.vars[elem.vars.size - extraParams[funIdx]! : elem.vars.size] }
 
 /--
 Given a matrix (row-major) of strings, arranges them in tabular form.

src/Lean/Elab/PreDefinition/WF/Main.lean

@@ -92,6 +92,7 @@ def wfRecursion (preDefs : Array PreDefinition) : TermElabM Unit := do
     let unaryPreDefs ← packDomain fixedPrefixSize preDefsDIte
     return (← packMutual fixedPrefixSize preDefs unaryPreDefs, fixedPrefixSize)
 
+  let extraParamss := preDefs.map (·.termination.extraParams)
   let wf ← do
     let (preDefsWith, preDefsWithout) := preDefs.partition (·.termination.termination_by?.isSome)
     if preDefsWith.isEmpty then
@@ -109,7 +110,7 @@ def wfRecursion (preDefs : Array PreDefinition) : TermElabM Unit := do
   let preDefNonRec ← forallBoundedTelescope unaryPreDef.type fixedPrefixSize fun prefixArgs type => do
     let type ← whnfForall type
     let packedArgType := type.bindingDomain!
-    elabWFRel preDefs unaryPreDef.declName fixedPrefixSize packedArgType wf fun wfRel => do
+    elabWFRel preDefs unaryPreDef.declName fixedPrefixSize packedArgType extraParamss wf fun wfRel => do
       trace[Elab.definition.wf] "wfRel: {wfRel}"
       let (value, envNew) ← withoutModifyingEnv' do
         addAsAxiom unaryPreDef

src/Lean/Elab/PreDefinition/WF/Rel.lean

@@ -24,15 +24,16 @@ private partial def unpackMutual (preDefs : Array PreDefinition) (mvarId : MVarI
   go 0 mvarId fvarId #[]
 
 private partial def unpackUnary (preDef : PreDefinition) (prefixSize : Nat) (mvarId : MVarId)
-    (fvarId : FVarId) (element : TerminationBy) : TermElabM MVarId := do
-  element.checkVars preDef.declName preDef.termination.extraParams
-  -- If `synthetic := false`, then this is user-provided, and should be interpreted
+    (fvarId : FVarId) (extraParams : Nat) (element : TerminationBy) : TermElabM MVarId := do
+  -- If elements.vars is ≤ extraParams, this is user-provided, and should be interpreted
   -- as left to right. Else it is provided by GuessLex, and may rename non-extra paramters as well.
   -- (Not pretty, but it works for now)
   let implicit_underscores :=
-    if element.synthetic then 0 else preDef.termination.extraParams - element.vars.size
+    if element.vars.size < extraParams then extraParams - element.vars.size else 0
   let varNames ← lambdaTelescope preDef.value fun xs _ => do
     let mut varNames ← xs.mapM fun x => x.fvarId!.getUserName
+    if element.vars.size > varNames.size then
+      throwErrorAt element.vars[varNames.size]! "too many variable names"
     for h : i in [:element.vars.size] do
       let varStx := element.vars[i]
       if let `($ident:ident) := varStx then
@@ -54,7 +55,8 @@ private partial def unpackUnary (preDef : PreDefinition) (prefixSize : Nat) (mva
   go 0 mvarId fvarId
 
 def elabWFRel (preDefs : Array PreDefinition) (unaryPreDefName : Name) (fixedPrefixSize : Nat)
-    (argType : Expr) (wf : TerminationWF) (k : Expr → TermElabM α) : TermElabM α := do
+    (argType : Expr) (extraParamss : Array Nat) (wf : TerminationWF) (k : Expr → TermElabM α) :
+    TermElabM α := do
   let α := argType
   let u ← getLevel α
   let expectedType := mkApp (mkConst ``WellFoundedRelation [u]) α
@@ -64,8 +66,8 @@ def elabWFRel (preDefs : Array PreDefinition) (unaryPreDefName : Name) (fixedPre
     let [fMVarId, wfRelMVarId, _] ← mainMVarId.apply (← mkConstWithFreshMVarLevels ``invImage) | throwError "failed to apply 'invImage'"
     let (d, fMVarId) ← fMVarId.intro1
     let subgoals ← unpackMutual preDefs fMVarId d
-    for (d, mvarId) in subgoals, element in wf, preDef in preDefs do
-      let mvarId ← unpackUnary preDef fixedPrefixSize mvarId d element
+    for (d, mvarId) in subgoals, extraParams in extraParamss, element in wf, preDef in preDefs do
+      let mvarId ← unpackUnary preDef fixedPrefixSize mvarId d extraParams element
       mvarId.withContext do
         let value ← Term.withSynthesize <| elabTermEnsuringType element.body (← mvarId.getType)
         mvarId.assign value

src/Lean/Elab/PreDefinition/WF/TerminationHint.lean

@@ -16,13 +16,6 @@ structure TerminationBy where
   ref       : Syntax
   vars      : TSyntaxArray [`ident, ``Lean.Parser.Term.hole]
   body      : Term
-  /--
-  If `synthetic := true`, then this `termination_by` clause was
-  generated by `GuessLex`, and `vars` refers to *all* parameters
-  of the function, not just the “extra parameters”.
-  Cf. Lean.Elab.WF.unpackUnary
-  -/
-  synthetic : Bool := false
   deriving Inhabited
 
 open Parser.Termination in
@@ -51,13 +44,14 @@ structure TerminationHints where
   ref : Syntax
   termination_by? : Option TerminationBy
   decreasing_by?  : Option DecreasingBy
-  /-- Here we record the number of parameters past the `:`. It is set by
-  `TerminationHints.rememberExtraParams` and used as folows:
-
-  * When we guess the termination argument in `GuessLex` and want to print it in surface-syntax
-    compatible form.
+  /-- Here we record the number of parameters past the `:`. This is
+  * `GuessLex` when there is no `termination_by` annotation, so that
+     we can print the guessed order in the right 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`).
+    parameters, we know which parameters they should apply to.
+
+  It it set in `TerminationHints.checkVars`, which is the place where we also check that the user
+  does not bind more extra parameters than present in the predefinition.
   -/
   extraParams : Nat
   deriving Inhabited
@@ -75,32 +69,20 @@ def TerminationHints.ensureNone (hints : TerminationHints) (reason : String): Co
   | .some _, .some _ =>
     logErrorAt hints.ref m!"unused termination hints, function is {reason}"
 
-/--
-Remembers `extraParams` for later use. Needs to happen early enough where we still know
-how many parameters came from the function header (`headerParams`).
--/
-def TerminationHints.rememberExtraParams (headerParams : Nat) (hints : TerminationHints)
-    (value : Expr) : TerminationHints :=
-  { hints with extraParams := value.getNumHeadLambdas - headerParams }
-
 /--
 Checks that `termination_by` binds at most as many variables are present in the outermost
-lambda of `value`, and throws appropriate errors.
+lambda of `value`, and logs (without failing) appropriate errors.
+
+Also remembers `extraParams` for later use.
 -/
-def TerminationBy.checkVars (funName : Name) (extraParams : Nat) (tb : TerminationBy) : MetaM Unit := do
-  unless tb.synthetic do
+def TerminationHints.checkVars (headerParams : Nat) (hints : TerminationHints) (value : Expr) :
+    MetaM TerminationHints := do
+  let extraParams := value.getNumHeadLambdas - headerParams
+  if let .some tb := hints.termination_by? then
     if tb.vars.size > extraParams then
-      let mut msg := m!"{parameters tb.vars.size} bound in `termination_by`, but the body of " ++
-        m!"{funName} only binds {parameters extraParams}."
-      if let `($ident:ident) := tb.vars[0]! then
-        if ident.getId.isSuffixOf funName then
-            msg := msg ++ m!" (Since Lean v4.6.0, the `termination_by` clause no longer " ++
-              "expects the function name here.)"
-      throwErrorAt tb.ref msg
-  where
-    parameters : Nat → MessageData
-    | 1 => "one parameter"
-    | n => m!"{n} parameters"
+      logErrorAt tb.ref <| m!"Too many extra parameters bound; the function definition only " ++
+        m!"has {extraParams} extra parameters."
+  return { hints with extraParams := extraParams }
 
 open Parser.Termination
 

src/Lean/Elab/Tactic/Induction.lean

@@ -79,7 +79,11 @@ namespace ElimApp
 structure Alt where
   /-- The short name of the alternative, used in `| foo =>` cases -/
   name      : Name
-  info      : ElimAltInfo
+  /-- A declaration corresponding to the inductive constructor.
+  (For custom recursors, the alternatives correspond to parameter names in the
+  recursor, so we may not have a declaration to point to.)
+  This is used for go-to-definition on the alternative name. -/
+  declName? : Option Name
   /-- The subgoal metavariable for the alternative. -/
   mvarId    : MVarId
   deriving Inhabited
@@ -159,8 +163,8 @@ partial def mkElimApp (elimInfo : ElimInfo) (targets : Array Expr) (tag : Name)
           let arg ← mkFreshExprSyntheticOpaqueMVar (← getArgExpectedType) (tag := appendTag tag binderName)
           let x   ← getBindingName
           modify fun s =>
-            let info := elimInfo.altsInfo[s.alts.size]!
-            { s with alts := s.alts.push ⟨x, info, arg.mvarId!⟩ }
+            let declName? := elimInfo.altsInfo[s.alts.size]!.declName?
+            { s with alts := s.alts.push ⟨x, declName?, arg.mvarId!⟩ }
           addNewArg arg
       loop
     | _ =>
@@ -282,7 +286,7 @@ where
     let mut usedWildcard := false
     let mut subgoals := #[] -- when alternatives are not provided, we accumulate subgoals here
     let mut altsSyntax := altsSyntax
-    for { name := altName, info, mvarId := altMVarId } in alts do
+    for { name := altName, declName?, mvarId := altMVarId } in alts do
       let numFields ← getAltNumFields elimInfo altName
       let mut isWildcard := false
       let altStx? ←
@@ -303,11 +307,7 @@ where
         match (← Cases.unifyEqs? numEqs altMVarId {}) with
         | none   => pure () -- alternative is not reachable
         | some (altMVarId', subst) =>
-          altMVarId ← if info.provesMotive then
-            (_, altMVarId) ← altMVarId'.introNP numGeneralized
-            pure altMVarId
-          else
-            pure altMVarId'
+          (_, altMVarId) ← altMVarId'.introNP numGeneralized
           for fvarId in toClear do
             altMVarId ← altMVarId.tryClear fvarId
           altMVarId.withContext do
@@ -333,7 +333,7 @@ where
           -- inside tacticInfo for the current alternative (in `evalAlt`)
           let addInfo : TermElabM Unit := do
             if (← getInfoState).enabled then
-              if let some declName := info.declName? then
+              if let some declName := declName? then
                 addConstInfo (getAltNameStx altStx) declName
               saveAltVarsInfo altMVarId altStx fvarIds
           let unusedAlt := do
@@ -345,11 +345,7 @@ where
           match (← Cases.unifyEqs? numEqs altMVarId {}) with
           | none => unusedAlt
           | some (altMVarId', subst) =>
-            altMVarId ← if info.provesMotive then
-              (_, altMVarId) ← altMVarId'.introNP numGeneralized
-              pure altMVarId
-            else
-              pure altMVarId'
+            (_, altMVarId) ← altMVarId'.introNP numGeneralized
             for fvarId in toClear do
               altMVarId ← altMVarId.tryClear fvarId
             altMVarId.withContext do

src/Lean/Elab/Tactic/Simp.lean

@@ -72,7 +72,6 @@ def Simp.DischargeWrapper.with (w : Simp.DischargeWrapper) (x : Option Simp.Disc
     finally
       set (← ref.get)
 
-/-- Construct a `Simp.DischargeWrapper` from the `Syntax` for a `simp` discharger. -/
 private def mkDischargeWrapper (optDischargeSyntax : Syntax) : TacticM Simp.DischargeWrapper := do
   if optDischargeSyntax.isNone then
     return Simp.DischargeWrapper.default
@@ -259,15 +258,8 @@ structure MkSimpContextResult where
    If `kind != SimpKind.simp`, the `discharge` option must be `none`
 
    TODO: generate error message if non `rfl` theorems are provided as arguments to `dsimp`.
-
-   The argument `simpTheorems` defaults to `getSimpTheorems`,
-   but allows overriding with an arbitrary mechanism to choose
-   the simp theorems besides those specified in the syntax.
-   Note that if the syntax includes `simp only`, the `simpTheorems` argument is ignored.
 -/
-def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (kind := SimpKind.simp)
-    (ignoreStarArg : Bool := false) (simpTheorems : CoreM SimpTheorems := getSimpTheorems) :
-    TacticM MkSimpContextResult := do
+def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (kind := SimpKind.simp) (ignoreStarArg : Bool := false) : TacticM MkSimpContextResult := do
   if !stx[2].isNone then
     if kind == SimpKind.simpAll then
       throwError "'simp_all' tactic does not support 'discharger' option"
@@ -278,7 +270,7 @@ def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (kind := SimpKind.simp)
   let simpTheorems ← if simpOnly then
     simpOnlyBuiltins.foldlM (·.addConst ·) ({} : SimpTheorems)
   else
-    simpTheorems
+    getSimpTheorems
   let simprocs ← if simpOnly then pure {} else Simp.getSimprocs
   let congrTheorems ← getSimpCongrTheorems
   let r ← elabSimpArgs stx[4] (eraseLocal := eraseLocal) (kind := kind) (simprocs := #[simprocs]) {

src/Lean/Meta/Tactic/ElimInfo.lean

@@ -11,15 +11,8 @@ namespace Lean.Meta
 
 structure ElimAltInfo where
   name      : Name
-  /-- A declaration corresponding to the inductive constructor.
-  (For custom recursors, the alternatives correspond to parameter names in the
-  recursor, so we may not have a declaration to point to.)
-  This is used for go-to-definition on the alternative name. -/
   declName? : Option Name
   numFields : Nat
-  /-- If `provesMotive := true`, then this alternative has `motive` as its conclusion.
-  Only for those alternatives the `induction` tactic should introduce reverted hypotheses.  -/
-  provesMotive : Bool
   deriving Repr, Inhabited
 
 /--
@@ -63,14 +56,13 @@ def getElimExprInfo (elimExpr : Expr) (baseDeclName? : Option Name := none) : Me
       if x != motive && !targets.contains x then
         let xDecl ← x.fvarId!.getDecl
         if xDecl.binderInfo.isExplicit then
-          let (numFields, provesMotive) ← forallTelescopeReducing xDecl.type fun args concl =>
-            pure (args.size, concl.getAppFn == motive)
+          let numFields ← forallTelescopeReducing xDecl.type fun args _ => pure args.size
           let name := xDecl.userName
           let declName? := do
             let base ← baseDeclName?
             let altDeclName := base ++ name
             if env.contains altDeclName then some altDeclName else none
-          altsInfo := altsInfo.push { name, declName?, numFields, provesMotive }
+          altsInfo := altsInfo.push { name, declName?, numFields }
     pure { elimExpr, elimType,  motivePos, targetsPos, altsInfo }
 
 def getElimInfo (elimName : Name) (baseDeclName? : Option Name := none) : MetaM ElimInfo := do

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean

@@ -40,7 +40,11 @@ def Value.toExpr (v : Value) : Expr :=
   unless e.isAppOfArity declName arity do return .continue
   let some v₁ ← fromExpr? e.appFn!.appArg! | return .continue
   let some v₂ ← fromExpr? e.appArg! | return .continue
-  evalPropStep e (op v₁.value v₂.value)
+  let d ← mkDecide e
+  if op v₁.value v₂.value then
+    return .done { expr := mkConst ``True, proof? := mkAppN (mkConst ``eq_true_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``true))] }
+  else
+    return .done { expr := mkConst ``False, proof? := mkAppN (mkConst ``eq_false_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``false))] }
 
 /-
 The following code assumes users did not override the `Fin n` instances for the arithmetic operators.

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean

@@ -47,7 +47,11 @@ def toExpr (v : Int) : Expr :=
   unless e.isAppOfArity declName arity do return .continue
   let some v₁ ← fromExpr? e.appFn!.appArg! | return .continue
   let some v₂ ← fromExpr? e.appArg! | return .continue
-  evalPropStep e (op v₁ v₂)
+  let d ← mkDecide e
+  if op v₁ v₂ then
+    return .done { expr := mkConst ``True, proof? := mkAppN (mkConst ``eq_true_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``true))] }
+  else
+    return .done { expr := mkConst ``False, proof? := mkAppN (mkConst ``eq_false_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``false))] }
 
 /-
 The following code assumes users did not override the `Int` instances for the arithmetic operators.

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 import Lean.Meta.Offset
 import Lean.Meta.Tactic.Simp.Simproc
-import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Util
 
 namespace Nat
 open Lean Meta Simp
@@ -29,7 +28,11 @@ def fromExpr? (e : Expr) : SimpM (Option Nat) := do
   unless e.isAppOfArity declName arity do return .continue
   let some n ← fromExpr? e.appFn!.appArg! | return .continue
   let some m ← fromExpr? e.appArg! | return .continue
-  evalPropStep e (op n m)
+  let d ← mkDecide e
+  if op n m then
+    return .done { expr := mkConst ``True, proof? := mkAppN (mkConst ``eq_true_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``true))] }
+  else
+    return .done { expr := mkConst ``False, proof? := mkAppN (mkConst ``eq_false_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``false))] }
 
 builtin_simproc [simp, seval] reduceSucc (Nat.succ _) := reduceUnary ``Nat.succ 1 (· + 1)
 

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean

@@ -41,7 +41,11 @@ def $toExpr (v : Value) : Expr :=
   unless e.isAppOfArity declName arity do return .continue
   let some n ← ($fromExpr e.appFn!.appArg!) | return .continue
   let some m ← ($fromExpr e.appArg!) | return .continue
-  evalPropStep e (op n.value m.value)
+  let d ← mkDecide e
+  if op n.value m.value then
+    return .done { expr := mkConst ``True, proof? := mkAppN (mkConst ``eq_true_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``true))] }
+  else
+    return .done { expr := mkConst ``False, proof? := mkAppN (mkConst ``eq_false_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``false))] }
 
 builtin_simproc [simp, seval] $(mkIdent `reduceAdd):ident ((_ + _ : $typeName)) := reduceBin ``HAdd.hAdd 6 (· + ·)
 builtin_simproc [simp, seval] $(mkIdent `reduceMul):ident ((_ * _ : $typeName)) := reduceBin ``HMul.hMul 6 (· * ·)

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Util.lean

@@ -1,22 +0,0 @@
-/-
-Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-import Lean.Meta.Tactic.Simp.Simproc
-
-namespace Lean.Meta.Simp
-
-/--
-Let `result` be the result of evaluating proposition `p`, return a `.done` step where
-the resulting expression is `True`(`False`) if `result is `true`(`false`), and the
-proof is uses `Decidable p` and the auxiliary theorems `eq_true_of_decide`/`eq_false_of_decide`.
--/
-def evalPropStep (p : Expr) (result : Bool) : SimpM Step := do
-  let d ← mkDecide p
-  if result then
-    return .done { expr := mkConst ``True, proof? := mkAppN (mkConst ``eq_true_of_decide) #[p, d.appArg!, (← mkEqRefl (mkConst ``true))] }
-  else
-    return .done { expr := mkConst ``False, proof? := mkAppN (mkConst ``eq_false_of_decide) #[p, d.appArg!, (← mkEqRefl (mkConst ``false))] }
-
-end Lean.Meta.Simp

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -556,12 +556,11 @@ def cacheResult (e : Expr) (cfg : Config) (r : Result) : SimpM Result := do
     modify fun s => { s with cache := s.cache.insert e { r with dischargeDepth } }
   return r
 
-partial def simpLoop (e : Expr) : SimpM Result := withIncRecDepth do
+partial def simpLoop (e : Expr) : SimpM Result := do
   let cfg ← getConfig
   if (← get).numSteps > cfg.maxSteps then
     throwError "simp failed, maximum number of steps exceeded"
   else
-    checkSystem "simp"
     modify fun s => { s with numSteps := s.numSteps + 1 }
     match (← pre e) with
     | .done r  => cacheResult e cfg r

src/Lean/Meta/Tactic/Split.lean

@@ -19,8 +19,7 @@ def getSimpMatchContext : MetaM Simp.Context :=
    }
 
 def simpMatch (e : Expr) : MetaM Simp.Result := do
-  let discharge? ← SplitIf.mkDischarge?
-  (·.1) <$> Simp.main e (← getSimpMatchContext) (methods := { pre, discharge? })
+  (·.1) <$> Simp.main e (← getSimpMatchContext) (methods := { pre, discharge? := SplitIf.discharge? })
 where
   pre (e : Expr) : SimpM Simp.Step := do
     unless (← isMatcherApp e) do
@@ -37,8 +36,7 @@ def simpMatchTarget (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
   applySimpResultToTarget mvarId target r
 
 private def simpMatchCore (matchDeclName : Name) (matchEqDeclName : Name) (e : Expr) : MetaM Simp.Result := do
-  let discharge? ← SplitIf.mkDischarge?
-  (·.1) <$> Simp.main e (← getSimpMatchContext) (methods := { pre, discharge? })
+  (·.1) <$> Simp.main e (← getSimpMatchContext) (methods := { pre, discharge? := SplitIf.discharge? })
 where
   pre (e : Expr) : SimpM Simp.Step := do
     if e.isAppOf matchDeclName then

src/Lean/Meta/Tactic/SplitIf.lean

@@ -31,17 +31,9 @@ def getSimpContext : MetaM Simp.Context :=
 
 /--
   Default `discharge?` function for `simpIf` methods.
-  It only uses hypotheses from the local context that have `index < numIndices`.
-  It is effective after a case-split.
-
-  Remark: when `simp` goes inside binders it adds new local declarations to the
-  local context. We don't want to use these local declarations since the cached result
-  would depend on them (see issue #3229). `numIndices` is the size of the local
-  context `decls` field before we start the simplifying the expression.
-
-  Remark: this function is now private, and we should use `mkDischarge?`.
--/
-private def discharge? (numIndices : Nat) (useDecide : Bool) : Simp.Discharge := fun prop => do
+  It only uses hypotheses from the local context. It is effective
+  after a case-split. -/
+def discharge? (useDecide := false) : Simp.Discharge := fun prop => do
   let prop ← instantiateMVars prop
   trace[Meta.Tactic.splitIf] "discharge? {prop}, {prop.notNot?}"
   if useDecide then
@@ -52,7 +44,7 @@ private def discharge? (numIndices : Nat) (useDecide : Bool) : Simp.Discharge :=
       if r.isConstOf ``true then
         return some <| mkApp3 (mkConst ``of_decide_eq_true) prop d.appArg! (← mkEqRefl (mkConst ``true))
   (← getLCtx).findDeclRevM? fun localDecl => do
-     if localDecl.index ≥ numIndices || localDecl.isAuxDecl then
+     if localDecl.isAuxDecl then
        return none
      else if (← isDefEq prop localDecl.type) then
        return some localDecl.toExpr
@@ -64,9 +56,6 @@ private def discharge? (numIndices : Nat) (useDecide : Bool) : Simp.Discharge :=
          else
            return none
 
-def mkDischarge? (useDecide := false) : MetaM Simp.Discharge :=
-  return discharge? (← getLCtx).numIndices useDecide
-
 /-- Return the condition of an `if` expression to case split. -/
 partial def findIfToSplit? (e : Expr) : Option Expr :=
   if let some iteApp := e.find? fun e => (e.isIte || e.isDIte) && !(e.getArg! 1 5).hasLooseBVars then
@@ -93,14 +82,14 @@ open SplitIf
 
 def simpIfTarget (mvarId : MVarId) (useDecide := false) : MetaM MVarId := do
   let mut ctx ← getSimpContext
-  if let (some mvarId', _) ← simpTarget mvarId ctx {} (← mvarId.withContext <| mkDischarge? useDecide) (mayCloseGoal := false) then
+  if let (some mvarId', _) ← simpTarget mvarId ctx {} (discharge? useDecide) (mayCloseGoal := false) then
     return mvarId'
   else
     unreachable!
 
 def simpIfLocalDecl (mvarId : MVarId) (fvarId : FVarId) : MetaM MVarId := do
   let mut ctx ← getSimpContext
-  if let (some (_, mvarId'), _) ← simpLocalDecl mvarId fvarId ctx {} (← mvarId.withContext <| mkDischarge?) (mayCloseGoal := false) then
+  if let (some (_, mvarId'), _) ← simpLocalDecl mvarId fvarId ctx {} discharge? (mayCloseGoal := false) then
     return mvarId'
   else
     unreachable!

src/Lean/Server/InfoUtils.lean

@@ -84,28 +84,7 @@ where go ctx? a
       | none => a
       | some ctx => f ctx i a
     ts.foldl (init := a) (go <| i.updateContext? ctx?)
-  | hole _ => a
-
-/--
-Fold an info tree as follows, while ensuring that the correct `ContextInfo` is supplied at each stage:
-
- * Nodes are combined with the initial value `init` using `f`, and the result is then combined with the children using a left fold
- * On InfoTree holes, we just return the initial value.
-
-This is like `InfoTree.foldInfo`, but it also passes the whole node to `f` instead of just the head.
--/
-partial def InfoTree.foldInfoTree (init : α) (f : ContextInfo → InfoTree → α → α) : InfoTree → α :=
-  go none init
-where
-  /-- `foldInfoTree.go` is like `foldInfoTree` but with an additional outer context parameter `ctx?`. -/
-  go ctx? a
-  | context ctx t => go (ctx.mergeIntoOuter? ctx?) a t
-  | t@(node i ts) =>
-    let a := match ctx? with
-      | none => a
-      | some ctx => f ctx t a
-    ts.foldl (init := a) (go <| i.updateContext? ctx?)
-  | hole _ => a
+  | _ => a
 
 def Info.isTerm : Info → Bool
   | ofTermInfo _ => true

src/Lean/Syntax.lean

@@ -530,5 +530,4 @@ def Stack.matches (stack : Syntax.Stack) (pattern : List $ Option SyntaxNodeKind
     |>.all id)
 
 end Syntax
-
 end Lean

src/library/trace.cpp

@@ -165,16 +165,16 @@ extern "C" object * lean_pp_expr(object * env, object * mctx, object * lctx, obj
 
 /*
 @[export lean_format_pretty]
-def pretty (f : Format) (w : Nat := defWidth) (indent : Nat := 0) (column := 0) : String :=
+def pretty (f : Format) (w : Nat := defWidth) : String :=
 */
-extern "C" object * lean_format_pretty(object * f, object * w, object * i, object * c);
+extern "C" object * lean_format_pretty(object * f, object * w);
 
 std::string pp_expr(environment const & env, options const & opts, local_ctx const & lctx, expr const & e) {
     options o = opts;
     // o = o.update(name{"pp", "proofs"}, true); --
     object_ref fmt = get_io_result<object_ref>(lean_pp_expr(env.to_obj_arg(), lean_mk_metavar_ctx(lean_box(0)), lctx.to_obj_arg(), o.to_obj_arg(),
                                                             e.to_obj_arg(), io_mk_world()));
-    string_ref str(lean_format_pretty(fmt.to_obj_arg(), lean_unsigned_to_nat(80), lean_unsigned_to_nat(0), lean_unsigned_to_nat(0)));
+    string_ref str(lean_format_pretty(fmt.to_obj_arg(), lean_unsigned_to_nat(80)));
     return str.to_std_string();
 }
 

tests/lean/decreasing_by.lean

@@ -77,7 +77,7 @@ end Ex4
 namespace Ex5
 -- Empty proof. Produces parse error and unsolved goals.
 def foo (n m : Nat) : Nat := foo n (dec2 m) + foo (dec1 n) 100
-termination_by (n, m)
+termination_by n m => (n, m)
 decreasing_by -- Error
 
 end Ex5

tests/lean/interactive/hover.lean

@@ -188,7 +188,7 @@ example : Nat → Nat → Nat := by
       --^ textDocument/hover
 
 def g (n : Nat) : Nat := g 0
-termination_by n
+termination_by n => n
 decreasing_by have n' := n; admit
                        --^ textDocument/hover
 

tests/lean/run/3229.lean

@@ -1,4 +0,0 @@
--- This example exposed a caching issue with the `discharge?` method used by the `split` tactic.
-example (b : Bool) :
-    (if b then 1 else if b then 1 else 0) = (if b then 1 else 0) := by
-  split <;> rfl

tests/lean/run/issue3212.lean

@@ -1,60 +0,0 @@
-namespace SillyParam
-
-set_option linter.unusedVariables false in
-theorem nat_rec_with_string (some_param : String) {motive : Nat → Prop}
-  (zero : motive .zero) (succ : ∀ n, motive n → motive (.succ n)) : ∀ n, motive n :=
-  @Nat.rec motive zero succ
-
-example (n m : Nat) (h : n ≠ zero) : Nat.add m n ≠ zero := by
-  induction n using nat_rec_with_string
-  case some_param =>
-    show String
-    exact "heh"
-  case zero => sorry
-  case succ => sorry
-
-end SillyParam
-
-namespace RestrictedMotive
-
-axiom Restriction : (Nat → Prop) → Prop
-
-axiom restricted_induction {motive : Nat → Prop} (h : Restriction motive)
-  (zero : motive .zero) (succ : ∀ n, motive n → motive (.succ n)) : ∀ n, motive n
-
-example (n m : Nat) (h : n ≠ zero) : Nat.add m n ≠ zero := by
-  induction n using restricted_induction
-  case h =>
-    show Restriction _
-    sorry
-  case zero => sorry
-  case succ => sorry
-
-end RestrictedMotive
-
-
-namespace DownInduction
-
-axiom down_induction {motive : Nat → Prop} (u : Nat) (x : Nat)
-  (le_u : x ≤ u) (start : motive u) (step : ∀ x, x < u → motive (x + 1) → motive x) : motive x
-
-example (n m : Nat) (h : m * m < 100) (h2 : n ≤ m) : n * n < 100 := by
-  induction n using down_induction
-  case u => exact m -- (could have used `using down_induction (u := m)` of course)
-  case le_u =>
-    -- This does not work as hoped for yet: `induction` will revert `h2`, because it mentions `n`,
-    -- but we’d like to keep it outside of the motive here.
-    sorry
-  case start => exact h
-  case step x hlt IH =>
-    have IH := IH hlt
-    sorry
-
--- Unfortunately, this doesn’t work either:
---  example (n m : Nat) (h : m * m < 100) (h2 : n ≤ m) : n * n < 100 := by
---    induction n using down_induction (le_u := h2)
--- because after this, the target `n` is no longer a universally qualified variable
---
--- This probably could be made to work with a bit more refactoring.
-
-end DownInduction

tests/lean/run/toFromJson.lean

@@ -2,13 +2,13 @@ import Lean
 
 open Lean
 
-declare_syntax_cat mjson
-syntax str : mjson
-syntax num : mjson
-syntax "{" (ident ": " mjson),* "}" : mjson
-syntax "[" mjson,* "]" : mjson
+declare_syntax_cat json
+syntax str : json
+syntax num : json
+syntax "{" (ident ": " json),* "}" : json
+syntax "[" json,* "]" : json
 
-syntax "json " mjson : term
+syntax "json " json : term
 
 /- declare a micro json parser, so we can write our tests in a more legible way. -/
 open Json in macro_rules

tests/lean/termination_by_vars.lean

@@ -117,19 +117,3 @@ def foo6 (v : Nat) := 5
     decreasing_by apply dec1_lt
 
 end InLetRec
-
-namespace ManyTooMany
-
-def tooManyVars (n : Nat) : Nat := tooManyVars (dec1 n)
-  termination_by x y z => x -- Error
-  decreasing_by apply dec1_lt
-
-end ManyTooMany
-
-namespace WithHelpfulComment
-
-def foo (n : Nat) : Nat := foo (dec1 n)
-  termination_by foo n => n -- Error
-  decreasing_by apply dec1_lt
-
-end WithHelpfulComment

tests/lean/termination_by_vars.lean.expected.out

@@ -1,9 +1,7 @@
-termination_by_vars.lean:14:2-14:23: error: one parameter bound in `termination_by`, but the body of Basic.tooManyVars only binds 0 parameters.
+termination_by_vars.lean:14:2-14:23: error: Too many extra parameters bound; the function definition only has 0 extra parameters.
 termination_by_vars.lean:23:2-23:21: error: no extra parameters bounds, please omit the `=>`
-termination_by_vars.lean:39:2-39:27: error: 3 parameters bound in `termination_by`, but the body of Basic.tooManyVariables2 only binds 2 parameters.
-termination_by_vars.lean:49:2-49:23: error: one parameter bound in `termination_by`, but the body of WithVariable.tooManyVars only binds 0 parameters.
+termination_by_vars.lean:39:2-39:27: error: Too many extra parameters bound; the function definition only has 2 extra parameters.
+termination_by_vars.lean:49:2-49:23: error: Too many extra parameters bound; the function definition only has 0 extra parameters.
 termination_by_vars.lean:58:2-58:21: error: no extra parameters bounds, please omit the `=>`
-termination_by_vars.lean:83:4-83:25: error: one parameter bound in `termination_by`, but the body of InLetRec.foo1.tooManyVars only binds 0 parameters.
+termination_by_vars.lean:83:4-83:25: error: Too many extra parameters bound; the function definition only has 0 extra parameters.
 termination_by_vars.lean:95:4-95:23: error: no extra parameters bounds, please omit the `=>`
-termination_by_vars.lean:124:2-124:27: error: 3 parameters bound in `termination_by`, but the body of ManyTooMany.tooManyVars only binds 0 parameters.
-termination_by_vars.lean:132:2-132:27: error: 2 parameters bound in `termination_by`, but the body of WithHelpfulComment.foo only binds 0 parameters. (Since Lean v4.6.0, the `termination_by` clause no longer expects the function name here.)