From 1f37cc7b412c27a9111c7ecdfb23e4cb00fe54e7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 29 Aug 2021 10:51:01 -0700 Subject: [PATCH] =?UTF-8?q?feat:=20add=20`next=20x=E2=82=81=20...=20x?= =?UTF-8?q?=E2=82=99=20=3D>=20tac`=20tactic?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Init/Notation.lean | 4 ++++ tests/lean/run/matchEqs.lean | 6 +++--- 2 files changed, 7 insertions(+), 3 deletions(-) diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean index 542d0c1e83..10da50fc31 100644 --- a/src/Init/Notation.lean +++ b/src/Init/Notation.lean @@ -279,6 +279,10 @@ syntax (name := constructor) "constructor" : tactic `case tag => tac` focuses on the goal with case name `tag` and solves it using `tac`, or else fails. `case tag x₁ ... xₙ => tac` additionally renames the `n` most recent hypotheses with inaccessible names to the given names. -/ syntax (name := case) "case " (ident <|> "_") (ident <|> "_")* " => " tacticSeq : tactic +/-- +`next => tac` focuses on the next goal solves it using `tac`, or else fails. +`next x₁ ... xₙ => tac` additionally renames the `n` most recent hypotheses with inaccessible names to the given names. -/ +macro "next " args:(ident <|> "_")* " => " tac:tacticSeq : tactic => `(tactic| case _ $(args.getArgs)* => $tac) /-- `allGoals tac` runs `tac` on each goal, concatenating the resulting goals, if any. -/ syntax (name := allGoals) "allGoals " tacticSeq : tactic diff --git a/tests/lean/run/matchEqs.lean b/tests/lean/run/matchEqs.lean index 872fc9a3b8..e7f5a07904 100644 --- a/tests/lean/run/matchEqs.lean +++ b/tests/lean/run/matchEqs.lean @@ -21,9 +21,9 @@ test% f.match_1 theorem ex (x : List Nat) : f x > 0 := by simp [f] induction x using f.match_1.splitter - case _ => simp [f.match_1.eq_1] - case _ => simp [f.match_1.eq_2] - case _ x h1 h2 => + next => simp [f.match_1.eq_1] + next x => simp [f.match_1.eq_2] + next x h1 h2 => rw [f.match_1.eq_3] . decide . exact h1