From e620cf3c8033ef9f10151137f62b7b8a40a70427 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 21 Aug 2024 20:49:51 +0200 Subject: [PATCH] =?UTF-8?q?fix:=20count=20let-bound=20variables=20in=20`in?= =?UTF-8?q?duction=20=E2=80=A6=20with`=20correctly=20(#5117)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This fixes #5058 and is a follow-up to #3505. --- src/Lean/Elab/Tactic/Induction.lean | 8 +++++++- tests/lean/run/indUsingLet.lean | 6 ++++++ 2 files changed, 13 insertions(+), 1 deletion(-) diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean index 83884708ef..374180b490 100644 --- a/src/Lean/Elab/Tactic/Induction.lean +++ b/src/Lean/Elab/Tactic/Induction.lean @@ -220,8 +220,14 @@ private def checkAltNames (alts : Array Alt) (altsSyntax : Array Syntax) : Tacti private def getNumExplicitFields (altMVarId : MVarId) (numFields : Nat) : MetaM Nat := altMVarId.withContext do let target ← altMVarId.getType withoutModifyingState do + -- The `numFields` count includes explicit, implicit and let-bound variables. + -- `forallMetaBoundTelescope` will reduce let-bindings, so we don't just count how many + -- explicit binders are in `bis`, but how many implicit ones. + -- If this turns out to be insufficient, then the real (and complicated) logic for which + -- arguments are explicit or implicit can be found in `introNImp`, let (_, bis, _) ← forallMetaBoundedTelescope target numFields - return bis.foldl (init := 0) fun r bi => if bi.isExplicit then r + 1 else r + let numImplicits := (bis.filter (!·.isExplicit)).size + return numFields - numImplicits private def saveAltVarsInfo (altMVarId : MVarId) (altStx : Syntax) (fvarIds : Array FVarId) : TermElabM Unit := withSaveInfoContext <| altMVarId.withContext do diff --git a/tests/lean/run/indUsingLet.lean b/tests/lean/run/indUsingLet.lean index 97056e9ba1..19a031c604 100644 --- a/tests/lean/run/indUsingLet.lean +++ b/tests/lean/run/indUsingLet.lean @@ -12,3 +12,9 @@ example (n : Nat) : n = n := by case zero => rfl case succ n _h _m _IH => rfl + +example (n : Nat) : n = n := by + induction n using some_induction with + | zero => rfl + | succ n _h _m _IH => + rfl