Markus Himmel 68f3fc6d5d feat: finite type conversions (Nat/Int/Fin/BitVec -> UIntX -> *) (#7340) ... This PR adds lemmas for iterated conversions between finite types which start with `Nat`/`Int`/`Fin`/`BitVec` and then go through `UIntX`.		2025-03-05 15:35:36 +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: IntX conversion lemmas (#7274)	2025-03-05 06:27:53 +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: finite type conversions (Nat/Int/Fin/BitVec -> UIntX -> *) (#7340)	2025-03-05 15:35:36 +00:00