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

feat(library/user_recursors): add is_user_defined_recursor predicate

Browse source
This commit is contained in:
Leonardo de Moura 2015-07-12 11:25:50 -04:00
parent f0e3eef38a
commit b0ac78c2cb
2 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/user_recursors.cpp
View file

@ -311,6 +311,10 @@ list<name> get_recursors_for(environment const & env, name const & I) {
return list<name>();
}
bool is_user_defined_recursor(environment const & env, name const & r) {
return recursor_ext::get_state(env).m_recursors.find(r) != nullptr;
}
has_recursors_pred::has_recursors_pred(environment const & env):
m_type2recursors(recursor_ext::get_state(env).m_type2recursors) {}

1
src/library/user_recursors.h
View file

@ -57,6 +57,7 @@ public:
environment add_user_recursor(environment const & env, name const & r, optional<unsigned> const & major_pos, bool persistent);
recursor_info get_recursor_info(environment const & env, name const & r);
list<name> get_recursors_for(environment const & env, name const & I);
bool is_user_defined_recursor(environment const & env, name const & r);
class has_recursors_pred {
name_map<list<name>> m_type2recursors;