experiment: reduce_nat no fvar check

dselsam · Jul 17, 2021 · 6ced516 · 6ced516
1 parent 0cf306e
commit 6ced516
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 8 deletions.
diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
@@ -573,7 +573,6 @@ template<typename F> optional<expr> type_checker::reduce_bin_nat_pred(F const &
 }
 
 optional<expr> type_checker::reduce_nat(expr const & e) {
-    if (has_fvar(e)) return none_expr();
     unsigned nargs = get_app_num_args(e);
     if (nargs == 1) {
         expr const & f = app_fn(e);
@@ -885,13 +884,11 @@ lbool type_checker::lazy_delta_reduction(expr & t_n, expr & s_n) {
         lbool r = is_def_eq_offset(t_n, s_n);
         if (r != l_undef) return r;
 
-        if (!has_fvar(t_n) && !has_fvar(s_n)) {
-            if (auto t_v = reduce_nat(t_n)) {
-                return to_lbool(is_def_eq_core(*t_v, s_n));
-            } else if (auto s_v = reduce_nat(s_n)) {
-                return to_lbool(is_def_eq_core(t_n, *s_v));
-            }
-        }
+	if (auto t_v = reduce_nat(t_n)) {
+	    return to_lbool(is_def_eq_core(*t_v, s_n));
+	} else if (auto s_v = reduce_nat(s_n)) {
+	    return to_lbool(is_def_eq_core(t_n, *s_v));
+	}
 
         if (auto t_v = reduce_native(env(), t_n)) {
             return to_lbool(is_def_eq_core(*t_v, s_n));

diff --git a/tests/lean/run/reduceNatFVar.lean b/tests/lean/run/reduceNatFVar.lean
@@ -0,0 +1,2 @@
+def n : Nat := 100000000000
+example (h : True) : Nat.ble ((fun _ => n) h) n = true := rfl