lean4-htt/src/Init/Data/BitVec
Siddharth 8850f9e9aa
feat: BitVec.signExtend_eq_append_extractLsb' (#7454)
This PR implements the bitwuzla rule
[BV_SIGN_EXTEND_ELIM](https://github.com/bitwuzla/bitwuzla/blob/main/src/rewrite/rewrites_bv.cpp#L3638-L3663),
which rewrites a `signExtend x` as an `append` of the appropriate sign
bits, followed by the bits of `x`.

---------

Co-authored-by: Alex Keizer <alex@keizer.dev>
2025-03-12 15:40:23 +00:00
..
Basic.lean chore: cleanup duplicate theorems (#7113) 2025-02-18 01:46:12 +00:00
BasicAux.lean refactor: redefine unsigned fixed width integers in terms of BitVec (#5323) 2024-10-16 07:28:23 +00:00
Bitblast.lean feat: add BitVec.[toNat|toFin|toInt]_[sshiftRight|sshiftRight'] (#7104) 2025-03-11 09:51:37 +00:00
Folds.lean feat: make BitVec.getElem the simp normal form and use it in ext (#5498) 2025-02-16 00:04:56 +00:00
Lemmas.lean feat: BitVec.signExtend_eq_append_extractLsb' (#7454) 2025-03-12 15:40:23 +00:00