3dd12f85f0
This PR adds further `@[grind]` annotations for `Option`, as follow-up to the recent additions to the `Option` API in #8379 and #8298. **However**, I am concurrently investigating adding `attribute [grind cases] Option`, which will result in many (most?) of the annotations for `Option` being removed again. In any case, I'm going to merge this first, as if that is viable I would like to test that most/all the lemmas now marked with `@[grind]` are still provable by `grind`. |
||
|---|---|---|
| .. | ||
| experiments | ||
| field_normalization.lean | ||
| grind_palindrome.lean | ||
| module_normalization.lean | ||
| module_relations.lean | ||
| ordered_modules.lean | ||
| README.md | ||
| ring_normalization.lean | ||
Aspirational test cases for grind
These are not expected to work yet; we're collecting examples that we'd like to make work!