diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean index 61817ee05c..0e97615007 100644 --- a/src/Init/Data/BitVec/Basic.lean +++ b/src/Init/Data/BitVec/Basic.lean @@ -290,7 +290,7 @@ Lean convention that division by zero returns zero. Examples: * `(7#4).sdiv 2 = 3#4` -* `(-9#4).sdiv 2 = -4#4` +* `(-8#4).sdiv 2 = -4#4` * `(5#4).sdiv -2 = -2#4` * `(-7#4).sdiv (-2) = 3#4` -/