b4b878b2d0
This PR prevents `exact?` and `apply?` from suggesting tactics that correspond to correct proofs but do not elaborate, and it allows these tactics to suggest `expose_names` when needed. These tactics now indicate that a non-compiling term was generated but do not suggest that that term be inserted. `exact?` also no longer suggests that the user try `apply?` if no partial suggestions were found. This addresses part of #5407 but does not achieve the exact expected behavior therein (due to #6122). |
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lean-toolchain | ||