leanprover · wkrozowski · Mar 5, 2025 · Mar 4, 2025 · Mar 4, 2025 · Mar 5, 2025
diff --git a/src/Lean/Elab/PreDefinition/TerminationMeasure.lean b/src/Lean/Elab/PreDefinition/TerminationMeasure.lean
@@ -52,7 +52,6 @@ Elaborates a `TerminationBy` to an `TerminationMeasure`.
 def TerminationMeasure.elab (funName : Name) (type : Expr) (arity extraParams : Nat)
     (hint : TerminationBy) : TermElabM TerminationMeasure := withDeclName funName do
   assert! extraParams ≤ arity
-
   if h : hint.vars.size > extraParams then
     let mut msg := m!"{parameters hint.vars.size} bound in `termination_by`, but the body of " ++
       m!"{funName} only binds {parameters extraParams}."
@@ -64,7 +63,7 @@ def TerminationMeasure.elab (funName : Name) (type : Expr) (arity extraParams :
 
   -- Bring parameters before the colon into scope
   let r ← withoutErrToSorry <|
-    forallBoundedTelescope type (arity - extraParams) fun ys type' => do
+    forallBoundedTelescope (cleanupAnnotations := true) type (arity - extraParams) fun ys type' => do
       -- Bring the variables bound by `termination_by` into scope.
       elabFunBinders hint.vars (some type') fun xs type' => do
         -- Elaborate the body in this local environment

diff --git a/tests/lean/run/issue6531.lean b/tests/lean/run/issue6531.lean
@@ -0,0 +1,9 @@
+-- This used to cause
+-- error: The termination argument's type must not depend on the function's varying parameters
+
+def foo (as : Array Nat) (i := 0) (j := as.size - 1) : Array Nat :=
+  if j ≤ i then as
+  else
+    let newas := as.set! 0 0
+    foo newas (i+1) (j-1)
+termination_by j - i