chore: delete more parens around 0#w, 1#w

opencompl · Jun 8, 2024 · 9bc8d7d · 9bc8d7d
1 parent 33be7e5
commit 9bc8d7d
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean
@@ -619,7 +619,7 @@ theorem ofBool_append (msb : Bool) (lsbs : BitVec w) :
 That is, 2 to the power `i`.
 For the bitwise point of view, it has the `i`th bit as `1` and all other bits as `0`.
 -/
-def twoPow {w : Nat} (i : Nat) : BitVec w := (1#w) <<< i
+def twoPow {w : Nat} (i : Nat) : BitVec w := 1#w <<< i
 
 end bitwise
 

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
@@ -1138,7 +1138,7 @@ theorem BitVec.mul_one {x : BitVec w} : x * 1#w = x := by
   simp [toNat_mul, Nat.mod_eq_of_lt x.isLt]
 
 @[simp]
-theorem BitVec.mul_zero {x : BitVec w} : x * (0#w) = (0#w) := by
+theorem BitVec.mul_zero {x : BitVec w} : x * 0#w = 0#w := by
   apply eq_of_toNat_eq
   simp [toNat_mul]