lean4-htt/src/Init/Data/BitVec
Siddharth da9a536ffd
feat: BitVec.msb_sdiv (#8178)
This PR provides a compact formula for the MSB of the sdiv. Most of the
work in the PR involves handling the corner cases of division
overflowing (e.g. `intMin / -1 = intMin`)

---------

Co-authored-by: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com>
Co-authored-by: Tobias Grosser <github@grosser.es>
2025-06-19 09:08:04 +00:00
..
Basic.lean feat: add leading zero counter BitVec.clz and bitblaster circuit/infrastructure (#8546) 2025-06-18 15:50:04 +00:00
BasicAux.lean chore: remove prime from Fin.ofNat' (#8515) 2025-05-28 11:51:00 +00:00
Bitblast.lean feat: BitVec.msb_sdiv (#8178) 2025-06-19 09:08:04 +00:00
Bootstrap.lean chore: reorganize BitVec files (#8829) 2025-06-17 03:30:35 +00:00
Decidable.lean chore: reorganize BitVec files (#8829) 2025-06-17 03:30:35 +00:00
Folds.lean feat: do not export def bodies by default (#8221) 2025-05-15 12:16:54 +00:00
Lemmas.lean feat: BitVec.msb_sdiv (#8178) 2025-06-19 09:08:04 +00:00