New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - chore(data/finset/basic): Golf and compress #11987
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM! I'm not really sure this was a good use of your time, but I'd much rather see it in a separate PR like this than mixed in with another one.
A couple minor comments above about section headings and pi vs forall.
bors d+
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Don't worry. It didn't take me too long. bors merge |
* Move the `lattice` instance earlier so that it can be used to prove lemmas * Golf proofs * Compress statements within the style guidelines
Pull request successfully merged into master. Build succeeded: |
lattice
instance earlier so that it can be used to prove lemmasThis is the grown out of proportions no novelty part of #11982.