feat(kernel/inductive): expose 'get_elim_name' API

src/frontends/lean/inductive_cmd.cpp

@@ -131,7 +131,7 @@ struct inductive_cmd_fn {
     }
 
     name mk_rec_name(name const & n) {
-        return n + name("rec");
+        return ::lean::inductive::get_elim_name(n);
     }
 
     /** \brief Parse the name of an inductive datatype or introduction rule,

src/kernel/inductive/inductive.cpp

@@ -183,7 +183,7 @@ static environment update(environment const & env, inductive_env_ext const & ext
 }
 
 /**\ brief Return recursor name */
-static name get_elim_name(name const & n) {
+name get_elim_name(name const & n) {
     return n + name("rec");
 }
 

src/kernel/inductive/inductive.h

@@ -72,6 +72,9 @@ bool is_elim_meta_app(type_checker & tc, expr const & e);
     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);
+
+/** \brief Return the eliminator/recursor associated with an inductive datatype */
+name get_elim_name(name const & n);
 }
 void initialize_inductive_module();
 void finalize_inductive_module();