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

feat(library/type_context): mimic behavior of the kernel type_checker

Browse source
This commit is contained in:
Leonardo de Moura 2016-09-03 16:43:33 -07:00
parent dfc897eda6
commit 696b190a8d
2 changed files with 19 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/library/type_context.cpp
View file

@ -2005,6 +2005,18 @@ lbool type_context::is_def_eq_lazy_delta(expr & t, expr & s) {
s = whnf_core(*unfold_definition(s));
}
}
/* If we haven't reduced t nor s, and they do not contain metavariables,
then we try to use the definitional height to decide which one we will unfold
(i.e., we mimic the behavior of the kernel type checker. */
if (!progress && !has_expr_metavar(t) && !has_expr_metavar(s)) {
if (!d_t->is_theorem() && d_t->get_height() > d_s->get_height()) {
progress = true;
t = whnf_core(*unfold_definition(t));
} else if (!d_s->is_theorem() && d_t->get_height() < d_s->get_height()) {
progress = true;
s = whnf_core(*unfold_definition(s));
}
}
/* If we haven't reduced t nor s, then we reduce both IF the reduction is productive.
That is, the result of the reduction is not a recursor application. */
if (!progress) {

7
tests/lean/run/is_def_eq_perf_bug.lean Normal file
View file

@ -0,0 +1,7 @@
definition f (n : nat) : nat :=
if n = 100000 then 1 else 0
open tactic
example (n : nat) : f 100000 = (if (100000 : nat) = 100000 then 1 else 0) :=
by reflexivity