From fb5440a0746d4f2e91e8a9bcefcca4eb98ebebf4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 24 Jul 2020 15:45:01 -0700 Subject: [PATCH] fix: new frontend does not eagerly simplify universe level expressions 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. --- src/kernel/level.cpp | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/src/kernel/level.cpp b/src/kernel/level.cpp index 20266a4dc5..d18d037361 100644 --- a/src/kernel/level.cpp +++ b/src/kernel/level.cpp @@ -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 todo;