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

fix(library/equations_compiler/elim_match): missing case for is_complete_transition

Browse source
This commit is contained in:
Leonardo de Moura 2016-09-10 12:13:31 -07:00
parent da966eeba0
commit 96d27b6b8f
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/equations_compiler/elim_match.cpp
View file

@ -479,7 +479,7 @@ struct elim_match_fn {
/* Return true iff the next pattern of every equation is a constructor or variable,
and there are at least one equation where it is a variable and another where it is a
constructor. */
bool is_complete_transition(problem const & P) const {
bool is_complete_transition(problem const & P) {
bool has_variable = false;
bool has_constructor = false;
bool r = all_next_pattern(P, [&](expr const & p) {
@ -487,6 +487,8 @@ struct elim_match_fn {
has_variable = true; return true;
} else if (is_constructor_app(p)) {
has_constructor = true; return true;
} else if (is_value(p)) {
return true;
} else {
return false;
}