From 143b2b49c8bb6d0bdf7ac5719f1f106b95253222 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 6 Jun 2022 23:04:09 +0200 Subject: [PATCH] fix: induction: do not register `_` as binder in info tree --- src/Lean/Elab/Tactic/Induction.lean | 2 +- tests/lean/1196.lean | 9 +++++++++ tests/lean/1196.lean.expected.out | 0 3 files changed, 10 insertions(+), 1 deletion(-) create mode 100644 tests/lean/1196.lean create mode 100644 tests/lean/1196.lean.expected.out diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean index 4f98918355..368e6adcee 100644 --- a/src/Lean/Elab/Tactic/Induction.lean +++ b/src/Lean/Elab/Tactic/Induction.lean @@ -199,7 +199,7 @@ private def saveAltVarsInfo (altMVarId : MVarId) (altStx : Syntax) (fvarIds : Ar for fvarId in fvarIds do if !useNamesForExplicitOnly || (← getLocalDecl fvarId).binderInfo.isExplicit then if i < altVars.size then - Term.addLocalVarInfo altVars[i] (mkFVar fvarId) + Term.addTermInfo' (isBinder := altVars[i].isIdent) altVars[i] (mkFVar fvarId) i := i + 1 /-- diff --git a/tests/lean/1196.lean b/tests/lean/1196.lean new file mode 100644 index 0000000000..02de7f2e53 --- /dev/null +++ b/tests/lean/1196.lean @@ -0,0 +1,9 @@ +inductive T: Type +| mk: Nat -> T + +theorem T.zero_bad: T -> T +:= by { + intro H; + induction H with + | mk _ => exact T.mk 0 +} diff --git a/tests/lean/1196.lean.expected.out b/tests/lean/1196.lean.expected.out new file mode 100644 index 0000000000..e69de29bb2