max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: fix BitVec docstring typo (#11694)

Browse source 
Closes #11680
This commit is contained in:
Henrik Böving 2025-12-16 09:54:14 +01:00 • committed by GitHub
parent 49d4752bfd
commit bd5d750780
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Data/BitVec/Basic.lean
View file

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