max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library/equations_compiler/util): add helper method

Browse source
This commit is contained in:
Leonardo de Moura 2016-08-21 15:47:31 -07:00
parent 1ea3bc1683
commit 2d90c73546
2 changed files with 6 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/library/equations_compiler/util.cpp
View file

@ -150,9 +150,13 @@ bool eqns_env_interface::is_inductive(expr const & e) const {
return is_inductive(const_name(e));
}
optional<name> eqns_env_interface::is_constructor(name const & n) const {
return inductive::is_intro_rule(m_env, n);
}
optional<name> eqns_env_interface::is_constructor(expr const & e) const {
if (!is_constant(e)) return optional<name>();
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 {

1
src/library/equations_compiler/util.h
View file

@ -81,6 +81,7 @@ public:
bool is_inductive(name const & n) const;
bool is_inductive(expr const & e) const;
optional<name> is_constructor(name const & n) const;
optional<name> is_constructor(expr const & e) const;
unsigned get_inductive_num_params(name const & n) const;
unsigned get_inductive_num_indices(name const & n) const;