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

fix(kernel/converter): missing delay_check case

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-09 08:01:29 -07:00
parent 0af55beb56
commit 4986226e41
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/kernel/converter.cpp
View file

@ -495,7 +495,10 @@ struct default_converter : public converter {
if (has_expr_metavar(t_n) || has_expr_metavar(s_n)) {
d_t = is_delta(t_n);
d_s = is_delta(s_n);
delay_check = d_t && d_s && is_eqp(*d_t, *d_s);
if (d_t && d_s && is_eqp(*d_t, *d_s))
delay_check = true;
else if (may_reduce_later(t_n, c) && may_reduce_later(s_n, c))
delay_check = true;
}
// At this point, t_n and s_n are in weak head normal form (modulo meta-variables and proof irrelevance)