max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: add next x₁ ... xₙ => tac tactic

Browse source
This commit is contained in:
Leonardo de Moura 2021-08-29 10:51:01 -07:00
parent 3972f011ee
commit 1f37cc7b41
2 changed files with 7 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Init/Notation.lean
View file

@ -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

6
tests/lean/run/matchEqs.lean
View file

@ -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