From 2070ac849cc8121afa22b899b179110e9ec88639 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 20 Dec 2014 11:30:41 -0800 Subject: [PATCH] feat(library/util): add get_intro_rule_names Signed-off-by: Leonardo de Moura --- src/library/util.cpp | 12 ++++++++++++ src/library/util.h | 5 +++++ 2 files changed, 17 insertions(+) diff --git a/src/library/util.cpp b/src/library/util.cpp index 2ad2410a6..ce9ebb3d2 100644 --- a/src/library/util.cpp +++ b/src/library/util.cpp @@ -106,6 +106,18 @@ bool is_inductive_predicate(environment const & env, name const & n) { return is_zero(get_datatype_level(env.get(n).get_type())); } +void get_intro_rule_names(environment const & env, name const & n, buffer & result) { + if (auto decls = inductive::is_inductive_decl(env, n)) { + for (inductive::inductive_decl const & decl : std::get<2>(*decls)) { + if (inductive::inductive_decl_name(decl) == n) { + for (inductive::intro_rule const & ir : inductive::inductive_decl_intros(decl)) + result.push_back(inductive::intro_rule_name(ir)); + return; + } + } + } +} + expr instantiate_univ_param (expr const & e, name const & p, level const & l) { return instantiate_univ_params(e, to_list(p), to_list(l)); } diff --git a/src/library/util.h b/src/library/util.h index b8637b9d7..daf50a846 100644 --- a/src/library/util.h +++ b/src/library/util.h @@ -39,6 +39,11 @@ bool is_reflexive_datatype(type_checker & tc, name const & n); */ bool is_inductive_predicate(environment const & env, name const & n); +/** \brief Store in \c result the introduction rules of the given inductive datatype. + \remark this procedure does nothing if \c n is not an inductive datatype. +*/ +void get_intro_rule_names(environment const & env, name const & n, buffer & result); + /** \brief "Consume" Pi-type \c type. This procedure creates local constants based on the domain of \c type and store them in telescope. If \c binfo is provided, then the local constants are annoted with the given binder_info, otherwise the procedure uses the one attached in the domain.