From 5446df16091530359b0dc90b96db5c0fac37fb49 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 1 Jun 2017 17:28:52 -0700 Subject: [PATCH] feat(library/init/meta/interactive): add interactive `done` tactic --- library/init/meta/interactive.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index 2f94fc38f3..22a53d8c3a 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -849,5 +849,9 @@ tactic.by_contradiction >> return () meta def by_contra : tactic unit := tactic.by_contradiction >> return () +/-- Fail if there are unsolved goals. -/ +meta def done : tactic unit := +tactic.done + end interactive end tactic