diff --git a/src/library/coercion.cpp b/src/library/coercion.cpp
index 1d09c4230..d5d174bff 100644
--- a/src/library/coercion.cpp
+++ b/src/library/coercion.cpp
@@ -344,6 +344,12 @@ bool is_coercion(environment const & env, expr const & 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) {
     coercion_state const & ext = coercion_ext::get_state(env);
     return ext.m_coercion_info.contains(C);
diff --git a/src/library/coercion.h b/src/library/coercion.h
index 5ace91d83..2f239de8e 100644
--- a/src/library/coercion.h
+++ b/src/library/coercion.h
@@ -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. */
 bool has_coercions_from(environment const & env, name 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.
    The coercion is a unary function that takes a term of type (C_name.{l1 lk} t_1 ... t_n) and returns