feat: add rfl to bv_ring, add rfl to bv_bench

opencompl · Nov 15, 2024 · 6ecaf30 · 6ecaf30
1 parent 1694b03
commit 6ecaf30
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/SSA/Projects/InstCombine/TacticAuto.lean b/SSA/Projects/InstCombine/TacticAuto.lean
@@ -189,6 +189,7 @@ macro "bv_ring" : tactic =>
       simp (config := {failIfUnchanged := false}) only [← BitVec.allOnes_sub_eq_xor,
         ← BitVec.negOne_eq_allOnes]
       ring_nf
+      rfl
       done
     )
    )
@@ -282,6 +283,7 @@ macro "bv_bench": tactic =>
       (
         all_goals (
           tac_bench [
+            "rfl" : (rfl; done),
             "bv_bitwise" : (bv_bitwise; done),
             "bv_ac" : (bv_ac; done),
             "bv_distrib" : (bv_distrib; done),