lean4-htt/src/Init/Data/BitVec
Siddharth c517688f1d
feat: ushiftRight bitblasting (#4872)
This adds theorems `ushiftRight_rec_zero`, `ushiftRight_rec_succ`,
`ushiftRight_rec_eq`, and `shiftRight_eq_shiftRight_rec`.

---------

Co-authored-by: Tobias Grosser <github@grosser.es>
2024-07-31 21:44:06 +00:00
..
Basic.lean feat: BitVec.twoPow and lemmas, toward bitblasting multiplication for LeanSAT (#4417) 2024-06-23 22:37:02 +00:00
Bitblast.lean feat: ushiftRight bitblasting (#4872) 2024-07-31 21:44:06 +00:00
Folds.lean feat: equivalence of bit-vector negation and bitblasted negation (#3920) 2024-05-06 06:03:28 +00:00
Lemmas.lean feat: ushiftRight bitblasting (#4872) 2024-07-31 21:44:06 +00:00