From 8881517018017bf714c99a6df3f06586d3eba3b0 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Wed, 15 Nov 2023 12:55:06 -0500 Subject: [PATCH] fix: report goals in `induction` with parse error --- src/Lean/Elab/Tactic/Induction.lean | 2 +- tests/lean/interactive/plainGoal.lean | 13 +++++++++++++ tests/lean/interactive/plainGoal.lean.expected.out | 9 +++++++++ 3 files changed, 23 insertions(+), 1 deletion(-) diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean index 1e1a0fcbd1..a3d8ee1fd0 100644 --- a/src/Lean/Elab/Tactic/Induction.lean +++ b/src/Lean/Elab/Tactic/Induction.lean @@ -264,7 +264,6 @@ def reorderAlts (alts : Array Alt) (altsSyntax : Array Syntax) : Array Alt := Id def evalAlts (elimInfo : ElimInfo) (alts : Array Alt) (optPreTac : Syntax) (altsSyntax : Array Syntax) (initialInfo : Info) (numEqs : Nat := 0) (numGeneralized : Nat := 0) (toClear : Array FVarId := #[]) : TacticM Unit := do - checkAltNames alts altsSyntax let hasAlts := altsSyntax.size > 0 if hasAlts then -- default to initial state outside of alts @@ -276,6 +275,7 @@ def evalAlts (elimInfo : ElimInfo) (alts : Array Alt) (optPreTac : Syntax) (alts else go where go := do + checkAltNames alts altsSyntax let alts := reorderAlts alts altsSyntax let hasAlts := altsSyntax.size > 0 let mut usedWildcard := false diff --git a/tests/lean/interactive/plainGoal.lean b/tests/lean/interactive/plainGoal.lean index 2b6c78aed3..207a3da1bb 100644 --- a/tests/lean/interactive/plainGoal.lean +++ b/tests/lean/interactive/plainGoal.lean @@ -134,3 +134,16 @@ example : True ∧ False := by · -- --^ $/lean/plainGoal --^ $/lean/plainGoal + +section + +example : True := by induction 1 with + --^ $/lean/plainGoal + +example : True := by induction 1 with | + --^ $/lean/plainGoal + +example : True := by induction 1 with done + --^ $/lean/plainGoal + +end diff --git a/tests/lean/interactive/plainGoal.lean.expected.out b/tests/lean/interactive/plainGoal.lean.expected.out index 70565ea534..2e8a471fb1 100644 --- a/tests/lean/interactive/plainGoal.lean.expected.out +++ b/tests/lean/interactive/plainGoal.lean.expected.out @@ -170,3 +170,12 @@ null {"textDocument": {"uri": "file://plainGoal.lean"}, "position": {"line": 133, "character": 4}} {"rendered": "```lean\ncase left\n⊢ True\n```", "goals": ["case left\n⊢ True"]} +{"textDocument": {"uri": "file://plainGoal.lean"}, + "position": {"line": 139, "character": 34}} +{"rendered": "```lean\nx✝ : Nat\n⊢ True\n```", "goals": ["x✝ : Nat\n⊢ True"]} +{"textDocument": {"uri": "file://plainGoal.lean"}, + "position": {"line": 142, "character": 34}} +{"rendered": "```lean\nx✝ : Nat\n⊢ True\n```", "goals": ["x✝ : Nat\n⊢ True"]} +{"textDocument": {"uri": "file://plainGoal.lean"}, + "position": {"line": 145, "character": 34}} +{"rendered": "```lean\nx✝ : Nat\n⊢ True\n```", "goals": ["x✝ : Nat\n⊢ True"]}