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

feat(library/relation_manager): add auxiliary functions

Browse source
This commit is contained in:
Leonardo de Moura 2015-05-27 12:07:06 -07:00
parent 4867dba175
commit 77f742ae8e
2 changed files with 9 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/relation_manager.cpp
View file

@ -226,6 +226,10 @@ optional<std::tuple<name, name, unsigned>> get_trans_extra_info(environment cons
}
}
bool is_subst_relation(environment const & env, name const & op) {
return rel_ext::get_state(env).m_subst_table.contains(op);
}
optional<name> get_refl_info(environment const & env, name const & op) {
if (auto it = get_refl_extra_info(env, op))
return optional<name>(std::get<0>(*it));

5
src/library/relation_manager.h
View file

@ -41,6 +41,11 @@ optional<std::tuple<name, name, unsigned>> get_trans_extra_info(environment cons
optional<name> get_refl_info(environment const & env, name const & op);
optional<name> get_symm_info(environment const & env, name const & op);
optional<name> get_trans_info(environment const & env, name const & op);
bool is_subst_relation(environment const & env, name const & op);
inline bool is_trans_relation(environment const & env, name const & op) { return static_cast<bool>(get_trans_info(env, op)); }
inline bool is_symm_relation(environment const & env, name const & op) { return static_cast<bool>(get_symm_info(env, op)); }
inline bool is_refl_relation(environment const & env, name const & op) { return static_cast<bool>(get_refl_info(env, op)); }
void initialize_relation_manager();
void finalize_relation_manager();
}