refactor(library/util,util): move is_internal_name to util/

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));

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);

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();

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();
 }