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

feat(library/coercion): add has_coercions_to function

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-26 18:38:27 -07:00
parent b11e1a5f34
commit ed299c0914
2 changed files with 8 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/library/coercion.cpp
View file

@ -344,6 +344,12 @@ bool is_coercion(environment const & env, expr const & f) {
return is_constant(f) && is_coercion(env, const_name(f)); return is_constant(f) && is_coercion(env, const_name(f));
} }
bool has_coercions_to(environment const & env, name const & D) {
coercion_state const & ext = coercion_ext::get_state(env);
auto it = ext.m_to.find(coercion_class::mk_user(D));
return it && !is_nil(*it);
}
bool has_coercions_from(environment const & env, name const & C) { bool has_coercions_from(environment const & env, name const & C) {
coercion_state const & ext = coercion_ext::get_state(env); coercion_state const & ext = coercion_ext::get_state(env);
return ext.m_coercion_info.contains(C); return ext.m_coercion_info.contains(C);

2
src/library/coercion.h
View file

@ -43,6 +43,8 @@ bool is_coercion(environment const & env, expr const & f);
/** \brief Return true iff the given environment has coercions from a user-class named \c C. */ /** \brief Return true iff the given environment has coercions from a user-class named \c C. */
bool has_coercions_from(environment const & env, name const & C); bool has_coercions_from(environment const & env, name const & C);
bool has_coercions_from(environment const & env, expr const & C); bool has_coercions_from(environment const & env, expr const & C);
/** \brief Return true iff the given environment has coercions to a user-class named \c D. */
bool has_coercions_to(environment const & env, name const & D);
/** /**
\brief Return a coercion (if it exists) from (C_name.{l1 lk} t_1 ... t_n) to the class named D. \brief Return a coercion (if it exists) from (C_name.{l1 lk} t_1 ... t_n) to the class named D.
The coercion is a unary function that takes a term of type (C_name.{l1 lk} t_1 ... t_n) and returns The coercion is a unary function that takes a term of type (C_name.{l1 lk} t_1 ... t_n) and returns