diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean index 28edd333e76e..37ae83c0e1c8 100644 --- a/src/Init/Data/BitVec/Basic.lean +++ b/src/Init/Data/BitVec/Basic.lean @@ -269,8 +269,8 @@ Return the absolute value of a signed bitvector. protected def abs (x : BitVec n) : BitVec n := if x.msb then .neg x else x /-- -Multiplication for bit vectors. This can be interpreted as either signed or unsigned negation -modulo `2^n`. +Multiplication for bit vectors. This can be interpreted as either signed or unsigned +multiplication modulo `2^n`. SMT-Lib name: `bvmul`. -/