Siddharth bc6188a70a feat: BitVec.twoPow and lemmas, toward bitblasting multiplication for LeanSAT (#4417) ... We add a new definition `BitVec.twoPow w i` to represent `(1#w <<< i)`. This expression is used to test bits when building the multiplication bitblaster. Patch 1/?, being peeled from https://github.com/opencompl/lean4/pull/6. --------- Co-authored-by: Tobias Grosser <github@grosser.es>		2024-06-23 22:37:02 +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: bitblasting theorems for signed comparisons (#4201)	2024-05-23 01:24:04 +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: BitVec.twoPow and lemmas, toward bitblasting multiplication for LeanSAT (#4417)	2024-06-23 22:37:02 +00:00