Vlad Tsyrklevich ca96ea331e feat: teach bv_normalize to rewrite subtractions to additions (#6890) ... This PR teaches bv_normalize to replace subtractions on one side of an equality with an addition on the other side, this re-write eliminates a not + addition in the normalized form so it is easier on the solver. Note that I also make a point to normalize (1 + ~~~x) to (~~~x + 1) to limit the amount of boilerplate symmetry theorems we require.		2025-02-01 10:56:54 +00:00
..
bench	test: identifier completion benchmark (#6796)	2025-01-27 19:31:32 +00:00
compiler
elabissues
ir
lean	feat: teach bv_normalize to rewrite subtractions to additions (#6890)	2025-02-01 10:56:54 +00:00
pkg
playground	feat: align take/drop/extract across List/Array/Vector (#6860)	2025-01-30 01:24:25 +00:00
plugin
simpperf
.gitignore
common.sh
lean-toolchain