Comment about sdiv in Init/Data/BitVec.lean is misleading

Open aqjune-aws opened this issue 2 months ago • 0 comments

https://github.com/leanprover/lean4/blob/082c65f22691b7e65158afd8fc8e8358527ae65c/src/Init/Data/BitVec/Basic.lean#L292-L295

In these lines, -9 is out of bounds of a bit-vector with 4 bits. If #4 means something else, it must be clarified.

Dec 15 '25 07:12 aqjune-aws