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

chore: missing !

Browse source
This commit is contained in:
Leonardo de Moura 2021-07-23 16:04:02 -07:00
parent 57b4b8ad1b
commit 3d402eda3f
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/kernel/type_checker.cpp
View file

@ -825,7 +825,7 @@ auto type_checker::lazy_delta_reduction_step(expr & t_n, expr & s_n) -> reductio
} else if (c > 0) {
s_n = whnf_core(*unfold_definition(s_n));
} else {
if (is_app(t_n) && is_app(s_n) && is_eqp(*d_t, *d_s) && d_t->get_hints().is_abbrev()) {
if (is_app(t_n) && is_app(s_n) && is_eqp(*d_t, *d_s) && !d_t->get_hints().is_abbrev()) {
// Optimization:
// We try to check if their arguments are definitionally equal.
// If they are, then t_n and s_n must be definitionally equal, and we can