From 7cbee83a8a88e133d71df8f5f0c65ec185c05d0c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 3 Nov 2020 12:33:38 -0800
Subject: [PATCH] feat: add `try` tactic

---
 src/Init/Tactics.lean            | 2 ++
 tests/lean/run/newfrontend1.lean | 6 ++----
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index e73feafcbb..5b9fcab909 100644
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -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)
diff --git a/tests/lean/run/newfrontend1.lean b/tests/lean/run/newfrontend1.lean
index 8e093ba641..0096e3fcec 100644
--- a/tests/lean/run/newfrontend1.lean
+++ b/tests/lean/run/newfrontend1.lean
@@ -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;