diff --git a/src/kernel/inductive/inductive.cpp b/src/kernel/inductive/inductive.cpp
index dc9ab906e..e2ecaff4d 100644
--- a/src/kernel/inductive/inductive.cpp
+++ b/src/kernel/inductive/inductive.cpp
@@ -182,6 +182,11 @@ static environment update(environment const & env, inductive_env_ext const & ext
     return env.update(g_ext->m_ext_id, std::make_shared<inductive_env_ext>(ext));
 }
 
+/**\ brief Return recursor name */
+static name get_elim_name(name const & n) {
+    return n + name("rec");
+}
+
 /** \brief Helper functional object for processing inductive datatype declarations. */
 struct add_inductive_fn {
     typedef std::unique_ptr<type_checker> type_checker_ptr;
@@ -630,7 +635,7 @@ struct add_inductive_fn {
     }
 
     /** \brief Return the name of the eliminator/recursor for \c d. */
-    name get_elim_name(inductive_decl const & d) { return inductive_decl_name(d) + name("rec"); }
+    name get_elim_name(inductive_decl const & d) { return ::lean::inductive::get_elim_name(inductive_decl_name(d)); }
 
     name get_elim_name(unsigned d_idx) { return get_elim_name(get_ith(m_decls, d_idx)); }
 
@@ -957,6 +962,15 @@ optional<inductive_decls> is_inductive_decl(environment const & env, name const
         return optional<inductive_decls>();
 }
 
+optional<unsigned> get_num_indices(environment const & env, name const & n) {
+    inductive_env_ext const & ext = get_extension(env);
+    if (auto it = ext.m_elim_info.find(get_elim_name(n))) {
+        return optional<unsigned>(it->m_num_indices);
+    } else {
+        return optional<unsigned>();
+    }
+}
+
 optional<name> is_intro_rule(environment const & env, name const & n) {
     inductive_env_ext const & ext = get_extension(env);
     if (auto it = ext.m_intro_info.find(n))
diff --git a/src/kernel/inductive/inductive.h b/src/kernel/inductive/inductive.h
index a12c56c63..86d0ab390 100644
--- a/src/kernel/inductive/inductive.h
+++ b/src/kernel/inductive/inductive.h
@@ -67,6 +67,11 @@ optional<name> is_elim_rule(environment const & env, name const & n);
 /** \brief Given the eliminator \c n, this function return the position of major premise */
 optional<unsigned> get_elim_major_idx(environment const & env, name const & n);
 bool is_elim_meta_app(type_checker & tc, expr const & e);
+
+/** \brief Return the number of indices in the given inductive datatype.
+    If \c n is not an inductive datatype in \c env, then return none.
+*/
+optional<unsigned> get_num_indices(environment const & env, name const & n);
 }
 void initialize_inductive_module();
 void finalize_inductive_module();