diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp
index ec0527165..06900e06d 100644
--- a/src/frontends/lean/inductive_cmd.cpp
+++ b/src/frontends/lean/inductive_cmd.cpp
@@ -404,11 +404,6 @@ struct inductive_cmd_fn {
         }
     }
 
-    // TODO(Leo): move to different file
-    static bool is_explicit(binder_info const & bi) {
-        return !bi.is_implicit() && !bi.is_strict_implicit() && !bi.is_inst_implicit();
-    }
-
     /** \brief Replace every occurrences of the inductive datatypes (in decls) in \c type with a local constant */
     expr fix_intro_rule_type(expr const & type, name_map<expr> const & ind_to_local) {
         unsigned nparams = 0; // number of explicit parameters
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index 38474d086..060246ff1 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -240,6 +240,10 @@ inline binder_info mk_inst_implicit_binder_info() { return binder_info(false, fa
 inline binder_info mk_cast_binder_info() { return binder_info(false, true); }
 inline binder_info mk_contextual_info(bool f) { return binder_info(false, false, f); }
 
+inline bool is_explicit(binder_info const & bi) {
+    return !bi.is_implicit() && !bi.is_strict_implicit() && !bi.is_inst_implicit();
+}
+
 bool operator==(binder_info const & i1, binder_info const & i2);
 inline bool operator!=(binder_info const & i1, binder_info const & i2) { return !(i1 == i2); }