diff --git a/src/library/compiler/llnf.cpp b/src/library/compiler/llnf.cpp
index f36481d0eb..6a402000d1 100644
--- a/src/library/compiler/llnf.cpp
+++ b/src/library/compiler/llnf.cpp
@@ -163,33 +163,13 @@ class to_llnf_fn {
 
     name_generator & ngen() { return m_st.ngen(); }
 
-    optional<unsigned> is_enum_type_core(name const & I) {
-        constant_info info  = env().get(I);
-        if (!info.is_inductive()) return optional<unsigned>();
-        unsigned n = 0;
-        for (name const & c : info.to_inductive_val().get_cnstrs()) {
-            if (is_pi(env().get(c).get_type()))
-                return optional<unsigned>();
-            if (n == std::numeric_limits<unsigned>::max())
-                return optional<unsigned>();
-            n++;
-        }
-        if (n < (1u << 8)) {
-            return optional<unsigned>(1);
-        } else if (n < (1u << 16)) {
-            return optional<unsigned>(2);
-        } else {
-            return optional<unsigned>(4);
-        }
-    }
-
     optional<unsigned> is_enum_type(expr const & type) {
         expr const & I = get_app_fn(type);
         if (!is_constant(I)) return optional<unsigned>();
         auto it = m_enum_cache.find(const_name(I));
         if (it != m_enum_cache.end())
             return it->second;
-        optional<unsigned> r = is_enum_type_core(const_name(I));
+        optional<unsigned> r = ::lean::is_enum_type(env(), const_name(I));
         m_enum_cache.insert(mk_pair(const_name(I), r));
         return r;
     }
diff --git a/src/library/compiler/util.cpp b/src/library/compiler/util.cpp
index 93b760615f..b017aea0a1 100644
--- a/src/library/compiler/util.cpp
+++ b/src/library/compiler/util.cpp
@@ -19,6 +19,26 @@ Author: Leonardo de Moura
 #include "library/compiler/util.h"
 
 namespace lean {
+optional<unsigned> is_enum_type(environment const & env, name const & I) {
+    constant_info info  = env.get(I);
+    if (!info.is_inductive()) return optional<unsigned>();
+    unsigned n = 0;
+    for (name const & c : info.to_inductive_val().get_cnstrs()) {
+        if (is_pi(env.get(c).get_type()))
+            return optional<unsigned>();
+        if (n == std::numeric_limits<unsigned>::max())
+            return optional<unsigned>();
+        n++;
+    }
+    if (n < (1u << 8)) {
+        return optional<unsigned>(1);
+    } else if (n < (1u << 16)) {
+        return optional<unsigned>(2);
+    } else {
+        return optional<unsigned>(4);
+    }
+}
+
 unsigned get_num_nested_lambdas(expr e) {
     unsigned r = 0;
     while (is_lambda(e)) {
diff --git a/src/library/compiler/util.h b/src/library/compiler/util.h
index ee7bc48076..b0c8da55a3 100644
--- a/src/library/compiler/util.h
+++ b/src/library/compiler/util.h
@@ -14,6 +14,12 @@ Author: Leonardo de Moura
 #include "library/util.h"
 
 namespace lean {
+/* Return the `some(n)` if `I` is the name of an inductive datatype that contains only constructors with 0-arguments,
+   and `n` is `1`, `2` or `4`, i.e., the number of bytes that should be used to store a value of this type.
+   Otherwise, it return `none`.
+   Remark: if the inductive datatype `I` has more than `2^32` constructors (very unlikely), the result is also `none`. */
+optional<unsigned> is_enum_type(environment const & env, name const & I);
+
 /* A "compiler" declaration `x := e` */
 typedef pair_ref<name, expr> comp_decl;
 typedef list_ref<comp_decl> comp_decls;