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

fix: new frontend does not eagerly simplify universe level expressions

Browse source 
Remark: even if we change the new frontend to simplify all universe
level expressions, we should not rely on this property in the kernel.
Reason: users may still create terms without this property.

Remark: this bug was preventing the kernel from accepting valid declarations.
This commit is contained in:
Leonardo de Moura 2020-07-24 15:45:01 -07:00
parent 9dc5ca66e2
commit fb5440a074
1 changed files with 1 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/kernel/level.cpp
View file

@ -522,10 +522,7 @@ level normalize(level const & l) {
case level_kind::IMax: {
auto l1 = normalize(imax_lhs(r));
auto l2 = normalize(imax_rhs(r));
if (!is_eqp(l1, imax_lhs(r)) || !is_eqp(l2, imax_rhs(r)))
return mk_succ(mk_imax(l1, l2), p.second);
else
return l;
return mk_imax(l1, l2);
}
case level_kind::Max: {
buffer<level> todo;