From 9a38aca8ec951f08752c8ed8d7bde01ae790369c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 9 Apr 2020 11:02:15 -0700
Subject: [PATCH] feat: add `evalFailIfSuccess`

---
 src/Init/Lean/Elab/Tactic/Basic.lean | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/src/Init/Lean/Elab/Tactic/Basic.lean b/src/Init/Lean/Elab/Tactic/Basic.lean
index 0e685f43e5..4f7b361dbd 100644
--- a/src/Init/Lean/Elab/Tactic/Basic.lean
+++ b/src/Init/Lean/Elab/Tactic/Basic.lean
@@ -298,6 +298,15 @@ fun stx => evalChoiceAux stx.getArgs 0
 @[builtinTactic skip] def evalSkip : Tactic :=
 fun stx => pure ()
 
+@[builtinTactic failIfSuccess] def evalFailIfSuccess : Tactic :=
+fun stx =>
+  let tactic := stx.getArg 1;
+  whenM
+    (catch
+      (do evalTactic tactic; pure true)
+      (fun _ => pure false))
+    (throwError stx ("tactic succeeded"))
+
 @[builtinTactic traceState] def evalTraceState : Tactic :=
 fun stx => do
   gs ← getUnsolvedGoals;