Update src/Init/Data/BitVec/Lemmas.lean

Co-authored-by: Kim Morrison <[email protected]>
opencompl · Jan 9, 2025 · 064aa35 · 064aa35
1 parent 82c9de4
commit 064aa35
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
@@ -2901,7 +2901,7 @@ theorem toNat_rotateLeft {x : BitVec w} {r : Nat} :
 
 /-! ## Rotate Right -/
 
-/--`rotateRight` is defined in terms of left and right shifts. -/
+/-- `rotateRight` is defined in terms of left and right shifts. -/
 theorem rotateRight_def {x : BitVec w} {r : Nat} :
   x.rotateRight r = (x >>> (r % w)) ||| (x <<< (w - r % w)) := by
   simp only [rotateRight, rotateRightAux]