add mul_one|one_mul

opencompl · Oct 27, 2024 · 743a58b · 743a58b
1 parent af063c4
commit 743a58b
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
@@ -195,6 +195,9 @@ theorem BitVec.add_const_right' (a b c : BitVec w) : (a + b) + c = (b + c) + a :
 attribute [bv_normalize] BitVec.mul_zero
 attribute [bv_normalize] BitVec.zero_mul
 
+attribute [bv_normalize] BitVec.mul_one
+attribute [bv_normalize] BitVec.one_mul
+
 attribute [bv_normalize] BitVec.shiftLeft_zero
 attribute [bv_normalize] BitVec.zero_shiftLeft