From bd5d750780b81a70984cbd8eae151cb369c9b1c7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Tue, 16 Dec 2025 09:54:14 +0100
Subject: [PATCH] chore: fix BitVec docstring typo (#11694)

Closes #11680
---
 src/Init/Data/BitVec/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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`
 -/