Fix missing case in the elaborator
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
4b7d4cf0d1
commit
4c27530930
1 changed files with 2 additions and 0 deletions
|
@ -123,6 +123,8 @@ class elaborator::imp {
|
|||
return level();
|
||||
} else if (is_type(e)) {
|
||||
return ty_level(e);
|
||||
} else if (e == Bool) {
|
||||
return level();
|
||||
} else {
|
||||
expr r = head_reduce_mmv(e, m_env, m_available_defs);
|
||||
if (!is_eqp(r, e)) {
|
||||
|
|
Loading…
Reference in a new issue