small change

opencompl · Nov 8, 2024 · 6878a2d · 6878a2d
1 parent 76b3e74
commit 6878a2d
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
@@ -1249,6 +1249,7 @@ theorem toNat_ushiftRight_eq_zero (x : BitVec w) (n : Nat) (hn : w ≤ n) :
 theorem toInt_ushiftRight_zero (x : BitVec w) :
     (x >>> 0).toInt = x.toInt := by simp
 
+
 @[simp]
 theorem toInt_ushiftRight_pos (x : BitVec w) (n : Nat) (hn : 0 < n) :
     (x >>> n).toInt = x.toNat >>> n := by