fix(library/tactic): add missing file

src/library/tactic/util.cpp

@@ -0,0 +1,30 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "library/aliases.h"
+#include "library/tactic/util.h"
+
+namespace lean {
+bool is_tactic_namespace_open(environment const & env) {
+    name apply_tac({"tactic", "apply"});
+    for (name const & a : get_expr_aliases(env, "apply")) {
+        if (a == apply_tac) {
+            // make sure the type is the expected one
+            if (auto d = env.find(a)) {
+                expr t = d->get_type();
+                if (is_pi(t)) {
+                    expr b = binding_body(t);
+                    if (!is_constant(b) || const_name(b) != "tactic")
+                        throw exception("tactic namespace declarations have been modified, "
+                                        "function 'tactic.apply' is expected to return a 'tactic'");
+                }
+            }
+            return true;
+        }
+    }
+    return false;
+}
+}

src/library/tactic/util.h

@@ -0,0 +1,12 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "kernel/environment.h"
+namespace lean {
+/** \brief Return true iff the tactic namespace is open in given environment. */
+bool is_tactic_namespace_open(environment const & env);
+}