From b558b5b91258fffd0f4bbe702ad3976ff0bc14cb Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Wed, 11 Oct 2023 20:36:28 -0400 Subject: [PATCH] perf: use quick_is_def_eq first --- src/kernel/type_checker.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 1527ee2e4b..281a17a6d1 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -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*