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

chore(compiler/elim_recursors): cleanup

Browse source
This commit is contained in:
Leonardo de Moura 2016-05-07 17:32:10 -07:00
parent 50fd4eb7bd
commit b54cd38b51
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/compiler/elim_recursors.cpp
View file

@ -230,9 +230,9 @@ protected:
return r;
}
bool is_nonrecursive_recursor(name const & n) {
bool is_recursive_recursor(name const & n) {
if (auto I_name = inductive::is_elim_rule(env(), n)) {
return !is_recursive_datatype(env(), *I_name);
return is_recursive_datatype(env(), *I_name);
}
return false;
}
@ -241,7 +241,7 @@ protected:
expr const & fn = get_app_fn(e);
if (is_constant(fn)) {
name const & n = const_name(fn);
if (inductive::is_elim_rule(env(), n) && !is_nonrecursive_recursor(n)) {
if (inductive::is_elim_rule(env(), n) && is_recursive_recursor(n)) {
return visit_recursor_app(e);
}
}