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

feat: add try tactic

Browse source
This commit is contained in:
Leonardo de Moura 2020-11-03 12:33:38 -08:00
parent aafa09ddcd
commit 7cbee83a8a
2 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Tactics.lean
View file

@ -16,3 +16,5 @@ syntax "repeat " tacticSeq : tactic
macro_rules
| `(tactic| repeat $seq) => `(tactic| (($seq); repeat $seq) <|> skip)
macro "try " t:tacticSeq : tactic => `(($t) <|> skip)

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

@ -134,8 +134,6 @@ by {
assumption
}
macro «try» t:tactic : tactic => `($t <|> skip)
theorem simple12 (x y z : Nat) : y = z → x = x → x = y → x = z :=
by {
intro h1; intro h2; intro h3;
@ -183,7 +181,7 @@ by {
theorem simple16 (x y z : Nat) : y = z → x = x → x = y → x = z :=
by {
intros h1 h2 h3;
try (clear x); -- should fail
try clear x; -- should fail
clear h2;
traceState;
apply Eq.trans;
@ -333,7 +331,7 @@ function α β a b => (a, b)
theorem simple20 (x y z : Nat) : y = z → x = x → x = y → x = z :=
by intros h1 h2 h3;
try (clear x); -- should fail
try clear x; -- should fail
clear h2;
traceState;
apply Eq.trans;