ef759d874f
This PR modifies `grind` to run with the `reducible` transparency setting. We do not want `grind` to unfold arbitrary terms during definitional equality tests. This PR also fixes several issues introduced by this change. The most common problem was the lack of a hint in proofs, particularly in those constructed using proof by reflection. This PR also introduces new sanity checks when `set_option grind.debug true` is used. |
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lean-toolchain | ||