diff --git a/src/library/coercion.cpp b/src/library/coercion.cpp index b8de49002..3c5647f4a 100644 --- a/src/library/coercion.cpp +++ b/src/library/coercion.cpp @@ -317,13 +317,13 @@ environment add_coercion(environment const & env, name const & f, io_state const return add_coercion(env, f, const_name(C), ios); } +bool is_coercion(environment const & env, name const & f) { + coercion_ext const & ext = get_extension(env); + return ext.m_coercions.contains(f); +} + bool is_coercion(environment const & env, expr const & f) { - if (is_constant(f)) { - coercion_ext const & ext = get_extension(env); - return ext.m_coercions.contains(const_name(f)); - } else { - return false; - } + return is_constant(f) && is_coercion(env, const_name(f)); } bool has_coercions_from(environment const & env, name const & C) { @@ -450,7 +450,12 @@ static int add_coercion(lua_State * L) { else return push_environment(L, add_coercion(to_environment(L, 1), to_name_ext(L, 2), to_name_ext(L, 3), to_io_state(L, 4))); } -static int is_coercion(lua_State * L) { return push_boolean(L, is_coercion(to_environment(L, 1), to_expr(L, 2))); } +static int is_coercion(lua_State * L) { + if (is_expr(L, 2)) + return push_boolean(L, is_coercion(to_environment(L, 1), to_expr(L, 2))); + else + return push_boolean(L, is_coercion(to_environment(L, 1), to_name_ext(L, 2))); +} static int has_coercions_from(lua_State * L) { if (is_expr(L, 2)) return push_boolean(L, has_coercions_from(to_environment(L, 1), to_expr(L, 2))); diff --git a/src/library/coercion.h b/src/library/coercion.h index 4c24becff..ab0d26f77 100644 --- a/src/library/coercion.h +++ b/src/library/coercion.h @@ -38,6 +38,7 @@ namespace lean { */ environment add_coercion(environment const & env, name & f, io_state const & ios); environment add_coercion(environment const & env, name const & f, name const & C, io_state const & ios); +bool is_coercion(environment const & env, name const & f); 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); diff --git a/tests/lua/coe1.lua b/tests/lua/coe1.lua index 4dfa147ab..a1cceebca 100644 --- a/tests/lua/coe1.lua +++ b/tests/lua/coe1.lua @@ -48,3 +48,10 @@ print("---------") for_each_coercion_user(env, function(C, D, f) print(tostring(C) .. " >-> " .. tostring(D) .. " : " .. tostring(f)) end) print(get_coercion(env, lst_nat, "dlst")) assert(env:type_check(get_coercion(env, lst_nat, "dlst"))) + +env:export("coe1_mod.olean") +local env2 = import_modules("coe1_mod") +print(get_coercion(env2, lst_nat, "dlst")) +assert(env2:type_check(get_coercion(env2, lst_nat, "dlst"))) +assert(is_coercion(env2, "vec2mat")) +assert(is_coercion(env2, "lst2vec"))