michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(kernel/level): add missing normalization rule

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-08 11:07:11 -07:00
parent 24227f0e51
commit 93e0599a0f
1 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/kernel/level.cpp
View file

@ -235,9 +235,11 @@ level mk_imax(level const & l1, level const & l2) {
if (is_not_zero(l2))
return mk_max(l1, l2);
else if (is_zero(l2))
return l2;
return l2; // imax u 0 = 0 for any u
else if (is_zero(l1))
return l2; // imax 0 u = u for any u
else if (l1 == l2)
return l1;
return l1; // imax u u = u
else
return level(new level_max_core(true, l1, l2));
}