Update src/Lean/Server/InfoUtils.lean

Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>

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/Array/Basic.lean

@@ -21,21 +21,6 @@ def mkArray {α : Type u} (n : Nat) (v : α) : Array α := {
   data := List.replicate n v
 }
 
-/--
-`ofFn f` with `f : Fin n → α` returns the list whose ith element is `f i`.
-```
-ofFn f = #[f 0, f 1, ... , f(n - 1)]
-``` -/
-def ofFn {n} (f : Fin n → α) : Array α := go 0 (mkEmpty n) where
-  /-- Auxiliary for `ofFn`. `ofFn.go f i acc = acc ++ #[f i, ..., f(n - 1)]` -/
-  go (i : Nat) (acc : Array α) : Array α :=
-    if h : i < n then go (i+1) (acc.push (f ⟨i, h⟩)) else acc
-termination_by n - i
-
-/-- The array `#[0, 1, ..., n - 1]`. -/
-def range (n : Nat) : Array Nat :=
-  n.fold (flip Array.push) (mkEmpty n)
-
 @[simp] theorem size_mkArray (n : Nat) (v : α) : (mkArray n v).size = n :=
   List.length_replicate ..
 
@@ -428,10 +413,6 @@ def map {α : Type u} {β : Type v} (f : α → β) (as : Array α) : Array β :
 def mapIdx {α : Type u} {β : Type v} (as : Array α) (f : Fin as.size → α → β) : Array β :=
   Id.run <| as.mapIdxM f
 
-/-- Turns `#[a, b]` into `#[(a, 0), (b, 1)]`. -/
-def zipWithIndex (arr : Array α) : Array (α × Nat) :=
-  arr.mapIdx fun i a => (a, i)
-
 @[inline]
 def find? {α : Type} (as : Array α) (p : α → Bool) : Option α :=
   Id.run <| as.findM? p
@@ -506,11 +487,6 @@ def elem [BEq α] (a : α) (as : Array α) : Bool :=
 def toList (as : Array α) : List α :=
   as.foldr List.cons []
 
-/-- Prepends an `Array α` onto the front of a list.  Equivalent to `as.toList ++ l`. -/
-@[inline]
-def toListAppend (as : Array α) (l : List α) : List α :=
-  as.foldr List.cons l
-
 instance {α : Type u} [Repr α] : Repr (Array α) where
   reprPrec a _ :=
     let _ : Std.ToFormat α := ⟨repr⟩
@@ -540,13 +516,6 @@ def concatMapM [Monad m] (f : α → m (Array β)) (as : Array α) : m (Array β
 def concatMap (f : α → Array β) (as : Array α) : Array β :=
   as.foldl (init := empty) fun bs a => bs ++ f a
 
-/-- Joins array of array into a single array.
-
-`flatten #[#[a₁, a₂, ⋯], #[b₁, b₂, ⋯], ⋯]` = `#[a₁, a₂, ⋯, b₁, b₂, ⋯]`
--/
-def flatten (as : Array (Array α)) : Array α :=
-  as.foldl (init := empty) fun r a => r ++ a
-
 end Array
 
 export Array (mkArray)

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/Init/Simproc.lean

@@ -94,7 +94,7 @@ macro_rules
 
 macro_rules
   | `($[$doc?:docComment]? $kind:attrKind simproc $[$pre?]? $[ [ $ids?:ident,* ] ]? $n:ident ($pattern:term) := $body) => do
-     let mut cmds := #[(← `($[$doc?:docComment]? simproc_decl $n ($pattern) := $body))]
+     let mut cmds := #[(← `(simproc_decl $n ($pattern) := $body))]
      let pushDefault (cmds : Array (TSyntax `command)) : MacroM (Array (TSyntax `command)) := do
        return cmds.push (← `(attribute [$kind simproc $[$pre?]?] $n))
      if let some ids := ids? then
@@ -116,13 +116,13 @@ macro_rules
 
 macro_rules
   | `($[$doc?:docComment]? $kind:attrKind builtin_simproc $[$pre?]? $n:ident ($pattern:term) := $body) => do
-    `($[$doc?:docComment]? builtin_simproc_decl $n ($pattern) := $body
+    `(builtin_simproc_decl $n ($pattern) := $body
       attribute [$kind builtin_simproc $[$pre?]?] $n)
   | `($[$doc?:docComment]? $kind:attrKind builtin_simproc $[$pre?]? [seval] $n:ident ($pattern:term) := $body) => do
-    `($[$doc?:docComment]? builtin_simproc_decl $n ($pattern) := $body
+    `(builtin_simproc_decl $n ($pattern) := $body
       attribute [$kind builtin_sevalproc $[$pre?]?] $n)
   | `($[$doc?:docComment]? $kind:attrKind builtin_simproc $[$pre?]? [simp, seval] $n:ident ($pattern:term) := $body) => do
-    `($[$doc?:docComment]? builtin_simproc_decl $n ($pattern) := $body
+    `(builtin_simproc_decl $n ($pattern) := $body
       attribute [$kind builtin_simproc $[$pre?]?] $n
       attribute [$kind builtin_sevalproc $[$pre?]?] $n)
 

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/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/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/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/simproc1.lean

@@ -5,15 +5,11 @@ def foo (x : Nat) : Nat :=
 
 open Lean Meta
 
-/-- doc-comment for reduceFoo -/
 simproc reduceFoo (foo _) := fun e => do
   unless e.isAppOfArity ``foo 1 do return .continue
   let some n ← Nat.fromExpr? e.appArg! | return .continue
   return .done { expr := mkNatLit (n+10) }
 
-#eval show MetaM _ from do
-  guard <| (← findDocString? (← getEnv) ``reduceFoo) = some "doc-comment for reduceFoo "
-
 example : x + foo 2 = 12 + x := by
   set_option simprocs false in fail_if_success simp
   simp_arith

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.)