From ee888e98726865ce056014eaacd31ab22e6abc0c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 17 Jun 2016 16:15:32 -0700
Subject: [PATCH] feat(library/init/meta/tactic): add 'now' tactic

---
 library/init/meta/tactic.lean | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index 06676e4c83..ae87320366 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -202,4 +202,9 @@ meta_definition all_goals (tac : tactic unit) : tactic unit :=
 do gs ← get_goals,
    all_goals_core tac gs []
 
+meta_definition now : tactic unit :=
+do n ← num_goals,
+   if n = 0 then skip
+   else fail "now tactic failed, there are unsolved goals"
+
 end tactic