Tobias Grosser 459c6e2a46 feat: BitVec.getElem_[sub|neg|sshiftRight'|abs] (#6126) ... This PR adds lemmas for extracting a given bit of a `BitVec` obtained via `sub`/`neg`/`sshiftRight'`/`abs`. --------- Co-authored-by: Kim Morrison <scott@tqft.net>		2024-11-21 07:01:11 +00:00
..
Basic.lean	chore: remove >6 month old deprecations (#6057)	2024-11-13 23:21:23 +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: BitVec.getElem_[sub|neg|sshiftRight'|abs] (#6126)	2024-11-21 07:01:11 +00:00
Folds.lean	chore: deprecate duplicated Fin.size_pos (#6025)	2024-11-11 04:06:13 +00:00
Lemmas.lean	feat: BitVec.getElem_[sub|neg|sshiftRight'|abs] (#6126)	2024-11-21 07:01:11 +00:00