feat: simplify trivial BitVec.replicate

leanprover · Aug 2, 2024 · eafed35 · eafed35
1 parent cbd897a
commit eafed35
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/LeanSAT/Tactics/Normalize/BitVec.lean b/LeanSAT/Tactics/Normalize/BitVec.lean
@@ -213,6 +213,8 @@ theorem BitVec.max_ult' (a : BitVec w) : (BitVec.ult (-1#w) a) = false := by
   rw [BitVec.lt_ult] at this
   simp [this]
 
+attribute [bv_normalize] BitVec.replicate_zero_eq
+
 end Normalize
 end BVDecide