From dd91d7e2e2b99498f9284fca04f178da1809fc4d Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Sun, 9 Mar 2025 01:13:14 +0100 Subject: [PATCH] fix: bv_omega to use -implicitDefEqProofs (#7387) This PR uses `-implicitDefEqProofs` in `bv_omega` to ensure it is not affected by the change in #7386. --------- Co-authored-by: Leonardo de Moura --- src/Init/Tactics.lean | 2 +- src/kernel/type_checker.cpp | 1 - 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index c3bd90299d..d9b4983704 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -1347,7 +1347,7 @@ syntax (name := omega) "omega" optConfig : tactic Currently the preprocessor is implemented as `try simp only [bitvec_to_nat] at *`. `bitvec_to_nat` is a `@[simp]` attribute that you can (cautiously) add to more theorems. -/ -macro "bv_omega" : tactic => `(tactic| (try simp only [bitvec_to_nat] at *) <;> omega) +macro "bv_omega" : tactic => `(tactic| (try simp -implicitDefEqProofs only [bitvec_to_nat] at *) <;> omega) /-- Implementation of `ac_nf` (the full `ac_nf` calls `trivial` afterwards). -/ syntax (name := acNf0) "ac_nf0" (location)? : tactic diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index dc4034e9ff..a58daf3824 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -618,7 +618,6 @@ template optional type_checker::reduce_bin_nat_pred(F const & } optional 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);