[Merged by Bors] - feat: quick version of mono tactic #1740
Conversation
|
This looks good to me, it's good to be able to tag lemmas with |
|
There should not be any duplicate syntaxes. When partially implementing a tactic, you should move the syntax line from |
fpvandoorn
added
awaiting-author
* inline from `register_label_attr` so that it doesn't create syntax
thorimur
added
awaiting-review
and removed
awaiting-author
|
✌️ hrmacbeth can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors d=thorimur |
|
✌️ thorimur can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
|
bors r+ |
This is an extremely partial port of the `mono*` tactic from Lean 3, implemented as a macro on top of `solve_by_elim`. The original `mono` had many configuration options and no documentation, so quite a bit is missing (and almost all the Lean 3 tests fail). Nonetheless I think it's worth merging this, because - it will get rid of errors in mathport output which come from lemmas being tagged with a nonexistent attribute `@[mono]` - in most mathlib3 uses of mono, only the basic version was used, not the various configuration options; thus I would guess that this version of `mono` will succeed fairly often in the port even though it fails nearly all the tests Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded:
|
bors
bot
changed the title
Restore most of the `mono` attribute now that #1740 is merged. I think I got all of the `mono`s.
This is an extremely partial port of the
mono*tactic from Lean 3, implemented as a macro on top ofsolve_by_elim. The originalmonohad many configuration options and no documentation, so quite a bit is missing (and almost all the Lean 3 tests fail). Nonetheless I think it's worth merging this, because@[mono]monowill succeed fairly often in the port even though it fails nearly all the testsNote: the
solve_by_elimbehavior is closer tomono*thanmono, so bothmonoandmono*are accepted here and, for now, mean the same thing.The full port of
monowill eventually work in every place that mathlib3 hadmono, so as long as nomono*is changed tomonobetween now and the full port ofmono, this conflation ofmono*andmonoshouldn't introduce many wrinkles. Any wrinkles it does introduce will be able to be easily corrected by changingmonotomono*.@[mono],@[mono left],@[mono right], and@[mono both]all just mean@[mono]for now.The full port of mono will be PR'd as #2323.