This PR fixes a bug in the equality propagation procedure in `grind.order`. Specifically, it affects the procedure that asserts equalities in the `grind` core state that are implied by (ring) inequalities in the `grind.order` module. closes #10622 |
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lake | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lakefile.toml | ||
| lean-toolchain | ||