Skip to content

Commit 82c9de4

Browse files
mhk119kim-em
andauthored
Update src/Init/Data/BitVec/Lemmas.lean
Co-authored-by: Kim Morrison <scott@tqft.net>
1 parent f6f9895 commit 82c9de4

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/Init/Data/BitVec/Lemmas.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2747,7 +2747,7 @@ theorem smod_zero {x : BitVec n} : x.smod 0#n = x := by
27472747

27482748
/--`rotateLeft` is defined in terms of left and right shifts. -/
27492749
theorem rotateLeft_def {x : BitVec w} {r : Nat} :
2750-
x.rotateLeft r = (x <<< (r % w)) ||| (x >>> (w - r % w)) := by
2750+
x.rotateLeft r = (x <<< (r % w)) ||| (x >>> (w - r % w)) := by
27512751
simp only [rotateLeft, rotateLeftAux]
27522752

27532753
/-- `rotateLeft` is invariant under `mod` by the bitwidth. -/

0 commit comments

Comments
 (0)