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

perf: use quick_is_def_eq first

Browse source
This commit is contained in:
Mario Carneiro 2023-10-11 20:36:28 -04:00 • committed by Leonardo de Moura
parent 57e23917b6
commit b558b5b912
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/kernel/type_checker.cpp
View file

@ -1003,6 +1003,8 @@ bool type_checker::is_def_eq_core(expr const & t, expr const & s) {
check_system("is_definitionally_equal");
bool use_hash = true;
lbool r = quick_is_def_eq(t, s, use_hash);
if (r != l_undef) return r == l_true;
// Very basic support for proofs by reflection. If `t` has no free variables and `s` is `Bool.true`,
// we fully reduce `t` and check whether result is `s`.
// TODO: add metadata to control whether this optimization is used or not.
@ -1011,7 +1013,6 @@ bool type_checker::is_def_eq_core(expr const & t, expr const & s) {
return true;
}
}
if (r != l_undef) return r == l_true;
/*
Apply whnf (without using delta-reduction or normalizer extensions), *and*