From ded1fe74c5ffa51e072d58293b0f7f030d90431a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 17 Jun 2016 16:18:15 -0700
Subject: [PATCH] refactor(library/init/meta/tactic): implement num_goals in
 Lean

---
 library/init/meta/tactic.lean       | 7 +++++--
 src/library/tactic/tactic_state.cpp | 5 -----
 2 files changed, 5 insertions(+), 7 deletions(-)

diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index ae87320366..df7dc72353 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -74,8 +74,6 @@ meta_constant unify_core    : expr → expr → transparency → tactic bool
 meta_constant get_local     : name → tactic expr
 /- Return the hypothesis in the main goal. Fail if tactic_state does not have any goal left. -/
 meta_constant local_context : tactic (list expr)
-/- Return the number of goals that need to be solved -/
-meta_constant num_goals     : tactic nat
 /-  Helper tactic for creating simple applications where some arguments are inferred using
     type inference.
 
@@ -166,6 +164,11 @@ do { ctx ← local_context,
 meta_definition dsimp : tactic unit :=
 target >>= defeq_simp >>= change
 
+/- Return the number of goals that need to be solved -/
+meta_definition num_goals     : tactic nat :=
+do gs ← get_goals,
+   return (length gs)
+
 /- We have to provide the instance argument `[has_mod nat]` because
    mod for nat was not defined yet -/
 meta_definition rotate_right (n : nat) [has_mod nat] : tactic unit :=
diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp
index 1b5755fdda..1447337bff 100644
--- a/src/library/tactic/tactic_state.cpp
+++ b/src/library/tactic/tactic_state.cpp
@@ -341,10 +341,6 @@ vm_obj tactic_local_context(vm_obj const & s0) {
     return mk_tactic_success(to_obj(to_list(r)), s);
 }
 
-vm_obj tactic_num_goals(vm_obj const & s) {
-    return mk_tactic_success(mk_vm_nat(length(to_tactic_state(s).goals())), to_tactic_state(s));
-}
-
 vm_obj tactic_to_expr(vm_obj const & qe, vm_obj const & s) {
     /* TODO(Leo): invoke elaborator */
     return mk_tactic_success(qe, to_tactic_state(s));
@@ -414,7 +410,6 @@ void initialize_tactic_state() {
     DECLARE_VM_BUILTIN(name({"tactic", "unify_core"}),        tactic_unify_core);
     DECLARE_VM_BUILTIN(name({"tactic", "get_local"}),         tactic_get_local);
     DECLARE_VM_BUILTIN(name({"tactic", "local_context"}),     tactic_local_context);
-    DECLARE_VM_BUILTIN(name({"tactic", "num_goals"}),         tactic_num_goals);
     DECLARE_VM_BUILTIN(name({"tactic", "to_expr"}),           tactic_to_expr);
     DECLARE_VM_BUILTIN(name({"tactic", "defeq_simp"}),        tactic_defeq_simp);
     DECLARE_VM_BUILTIN(name({"tactic", "rotate_left"}),       tactic_rotate_left);