Apply suggestions from code review

Co-authored-by: Tobias Grosser <github@grosser.es>
opencompl · Jul 27, 2024 · 6022cf9 · 6022cf9
1 parent b6e0b32
commit 6022cf9
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 3 deletions.
diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean
@@ -536,7 +536,6 @@ instance {n} : HShiftRight (BitVec m) (BitVec n) (BitVec m) := ⟨fun x y => x >
 
 def sshiftRight' (a : BitVec n) (s : BitVec m) : BitVec n := a.sshiftRight s.toNat
 
-
 /-- Auxiliary function for `rotateLeft`, which does not take into account the case where
 the rotation amount is greater than the bitvector width. -/
 def rotateLeftAux (x : BitVec w) (n : Nat) : BitVec w :=

diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean
@@ -453,7 +453,6 @@ theorem ushiftRight_rec_succ (x : BitVec w₁) (y : BitVec w₂) :
 theorem ushiftRight_eq' (x : BitVec w) (y : BitVec w₂) :
   x >>> y = x >>> y.toNat := by rfl
 
-
 @[simp]
 theorem BitVec.ushiftRight_zero (x : BitVec w) : x >>> 0 = x := by
   simp [bv_toNat]
@@ -503,7 +502,6 @@ theorem shiftRight_eq_shiftRight_rec (x : BitVec ℘) (y : BitVec w₂) :
   · simp [of_length_zero]
   · simp [ushiftRight_rec_eq]
 
-
 /- ### Arithmetic (sshiftRight) recurrence -/
 
 @[simp]