diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean
index e652f148081b..0e16c7bc1bf9 100644
--- a/src/Init/Data/BitVec/Basic.lean
+++ b/src/Init/Data/BitVec/Basic.lean
@@ -676,28 +676,28 @@ def ofBoolListLE : (bs : List Bool) → BitVec bs.length
 
 def not_overflow {w : Nat} (x : BitVec w) : Bool := x.toInt == - (2 ^ (w - 1))
 
-/-- Overflow predicate for unsigned addition modulo 2^m.
+/-- Overflow predicate for unsigned addition modulo 2^w.
 
   SMT-Lib name: `bvuaddo`.
 -/
 
 def uadd_overflow {w : Nat} (x y : BitVec w) : Bool := x.toNat + y.toNat ≥ 2 ^ w
 
-/-- Overflow predicate for signed addition on m-bit 2's complement.
+/-- Overflow predicate for signed addition on w-bit 2's complement.
 
   SMT-Lib name: `bvsaddo`.
 -/
 
 def sadd_overflow {w : Nat} (x y : BitVec w) : Bool := (x.toInt + y.toInt ≥ 2 ^ (w - 1)) || (x.toInt + y.toInt < - 2 ^ (w - 1))
 
-/-- Overflow predicate for unsigned multiplication modulo 2^m.
+/-- Overflow predicate for unsigned multiplication modulo 2^w.
 
   SMT-Lib name: `bvumulo`.
 -/
 
 def umul_overflow {w : Nat} (x y : BitVec w) : Bool := x.toNat * y.toNat ≥ 2 ^ w
 
-/-- Overflow predicate for signed multiplication on m-bit 2's complement.
+/-- Overflow predicate for signed multiplication on w-bit 2's complement.
 
   SMT-Lib name: `bvsmulo`.
 -/