michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/util): add get_intro_rule_names

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-12-20 11:30:41 -08:00
parent d9d822baa7
commit 2070ac849c
2 changed files with 17 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/library/util.cpp
View file

@ -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<name> & 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));
}

5
src/library/util.h
View file

@ -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<name> & 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.