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

chore: prepare to change case tactic

Browse source
This commit is contained in:
Leonardo de Moura 2021-05-01 19:53:44 -07:00
parent ba5d622e59
commit 93189e0fce
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Notation.lean
View file

@ -214,7 +214,7 @@ syntax (name := apply) "apply " term : tactic
syntax (name := exact) "exact " term : tactic
syntax (name := refine) "refine " term : tactic
syntax (name := refine') "refine' " term : tactic
syntax (name := case) "case " ident " => " tacticSeq : tactic
syntax (name := case) "case " ident (ident <|> "_")* " => " tacticSeq : tactic
syntax (name := allGoals) "allGoals " tacticSeq : tactic
syntax (name := focus) "focus " tacticSeq : tactic
syntax (name := skip) "skip" : tactic

2
src/Lean/Elab/Tactic/Basic.lean
View file

@ -541,7 +541,7 @@ def withCaseRef [Monad m] [MonadRef m] (arrow body : Syntax) (x : m α) : m α :
withRef (mkNullNode #[arrow, body]) x
@[builtinTactic «case»] def evalCase : Tactic
| `(tactic| case $tag =>%$arr $tac:tacticSeq) => do
| `(tactic| case $tag $hs* =>%$arr $tac:tacticSeq) => do
let tag := tag.getId
let gs ← getUnsolvedGoals
let some g ← findTag? gs tag | throwError "tag not found"