feat: only suggest `grind?` tactics that close the goal This PR makes `grind?` check each suggested tactic before showing it. Previously, only the generated `grind =>` script was checked, and it was suggested even when the check failed. Suggestions that do not close the goal are now reported in a warning instead of being suggested, and if none of them works, `grind?` suggests `grind` with the original configuration and parameters. `try?` uses the same check for the `grind only` suggestions it shows. It also adds the options `grind.debug.badAnchors`, `grind.debug.dropParams`, and `grind.debug.dropSteps`, which deliberately break the suggestions of `grind?`. They are for debugging and testing only, and are used to test the reporting of failing suggestions. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This is the repository for Lean 4.
See Install Lean.
Please read our Contribution Guidelines first.
See Building Lean.