From cc8eb83507c5cdfe4aece7348ada55d475134d1a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 6 Feb 2018 16:09:40 -0800
Subject: [PATCH] refactor(library/util,util): move is_internal_name to util/

---
 src/library/util.cpp | 10 ----------
 src/library/util.h   |  3 ---
 src/util/name.cpp    | 10 ++++++++++
 src/util/name.h      |  3 +++
 4 files changed, 13 insertions(+), 13 deletions(-)

diff --git a/src/library/util.cpp b/src/library/util.cpp
index 488c546940..e723f9c474 100644
--- a/src/library/util.cpp
+++ b/src/library/util.cpp
@@ -39,16 +39,6 @@ unsigned get_arity(expr type) {
     return r;
 }
 
-bool is_internal_name(name const & n) {
-    name it = n;
-    while (!it.is_anonymous()) {
-        if (!it.is_anonymous() && it.is_string() && it.get_string() && it.get_string()[0] == '_')
-            return true;
-        it = it.get_prefix();
-    }
-    return false;
-}
-
 optional<expr> is_optional_param(expr const & e) {
     if (is_app_of(e, get_opt_param_name(), 2)) {
         return some_expr(app_arg(e));
diff --git a/src/library/util.h b/src/library/util.h
index 1c2b0945c6..8e85df14d0 100644
--- a/src/library/util.h
+++ b/src/library/util.h
@@ -13,9 +13,6 @@ namespace lean {
 /** \brief Return the "arity" of the given type. The arity is the number of nested pi-expressions. */
 unsigned get_arity(expr type);
 
-/** \brief Return true if it is a lean internal name, i.e., the name starts with a `_` */
-bool is_internal_name(name const & n);
-
 optional<expr> is_optional_param(expr const & e);
 
 optional<expr_pair> is_auto_param(expr const & e);
diff --git a/src/util/name.cpp b/src/util/name.cpp
index 9de6ff96e1..67ef436214 100644
--- a/src/util/name.cpp
+++ b/src/util/name.cpp
@@ -546,6 +546,16 @@ name read_name(deserializer & d) {
     return d.get_extension<name_deserializer>(g_name_sd->m_deserializer_extid).read();
 }
 
+bool is_internal_name(name const & n) {
+    name it = n;
+    while (!it.is_anonymous()) {
+        if (!it.is_anonymous() && it.is_string() && it.get_string() && it.get_string()[0] == '_')
+            return true;
+        it = it.get_prefix();
+    }
+    return false;
+}
+
 void initialize_name() {
     g_anonymous = new name();
     g_name_sd   = new name_sd();
diff --git a/src/util/name.h b/src/util/name.h
index a151932d47..262ddd5e51 100644
--- a/src/util/name.h
+++ b/src/util/name.h
@@ -258,6 +258,9 @@ serializer & operator<<(serializer & s, name const & n);
 name read_name(deserializer & d);
 inline deserializer & operator>>(deserializer & d, name & n) { n = read_name(d); return d; }
 
+/** \brief Return true if it is a lean internal name, i.e., the name starts with a `_` */
+bool is_internal_name(name const & n);
+
 void initialize_name();
 void finalize_name();
 }