This PR ensures that `Nat.cast` and `Int.cast` of numerals are normalized by `grind`. It also adds a `simp` flag for controlling how bitvector literals are represented. By default, the bitvector simprocs use `BitVec.ofNat`. This representation is problematic for the `grind ring` and `grind cutsat` modules. The new flag allows the use of `OfNat.ofNat` and `Neg.neg` to represent literals, consistent with how they are represented for other commutative rings. Closes #9321 |
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lakefile.toml | ||
| lean-toolchain | ||