diff --git a/src/library/equations_compiler/util.cpp b/src/library/equations_compiler/util.cpp index 49cfde8bde..80a74ba39e 100644 --- a/src/library/equations_compiler/util.cpp +++ b/src/library/equations_compiler/util.cpp @@ -150,9 +150,13 @@ bool eqns_env_interface::is_inductive(expr const & e) const { return is_inductive(const_name(e)); } +optional eqns_env_interface::is_constructor(name const & n) const { + return inductive::is_intro_rule(m_env, n); +} + optional eqns_env_interface::is_constructor(expr const & e) const { if (!is_constant(e)) return optional(); - return inductive::is_intro_rule(m_env, const_name(e)); + return is_constructor(const_name(e)); } unsigned eqns_env_interface::get_inductive_num_params(name const & n) const { diff --git a/src/library/equations_compiler/util.h b/src/library/equations_compiler/util.h index 9debbb777f..775a6abdf6 100644 --- a/src/library/equations_compiler/util.h +++ b/src/library/equations_compiler/util.h @@ -81,6 +81,7 @@ public: bool is_inductive(name const & n) const; bool is_inductive(expr const & e) const; + optional is_constructor(name const & n) const; optional is_constructor(expr const & e) const; unsigned get_inductive_num_params(name const & n) const; unsigned get_inductive_num_indices(name const & n) const;