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

fix(library/old_default_converter): avoid underflow

Browse source
This commit is contained in:
Leonardo de Moura 2016-09-03 16:21:34 -07:00
parent 80607c8895
commit 01a2c32d38
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/old_default_converter.cpp
View file

@ -524,8 +524,8 @@ auto old_default_converter::lazy_delta_reduction_step(expr & t_n, expr & s_n, co
}
}
}
t_n = whnf_core(unfold_names(t_n, d_t->get_height() - 1));
s_n = whnf_core(unfold_names(s_n, d_s->get_height() - 1));
t_n = whnf_core(unfold_names(t_n, d_t->get_height() > 0 ? d_t->get_height() - 1 : 0));
s_n = whnf_core(unfold_names(s_n, d_s->get_height() > 0 ? d_s->get_height() - 1 : 0));
}
switch (quick_is_def_eq(t_n, s_n, cs)) {
case l_true: return reduction_status::DefEqual;