-
Notifications
You must be signed in to change notification settings - Fork 251
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] - feat: minimal port of Fintype #429
Conversation
Note: the commit convention for lean 4 no longer puts the file name in the commit message. |
It is intentional, although I don't mind nolinting the definitions if you think we should delay documenting it. (Use |
I made some minor style changes and golfed the proof of bors d+ |
✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with |
Thanks, looks great. bors merge |
This is a bare minimum port of the definitions of `Finset` / `Multiset` / `Fintype`. I am hoping that these are enough to port the `fin_cases` tactic. (i.e. replacing the unfinished work in #346, which still had sorries in the corresponding material) Where possible I have started by copying and pasting the output from `mathlib3port`. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Mario Carneiro <di.gama@gmail.com>
Pull request successfully merged into master. Build succeeded: |
- [x] depends on: #429 Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
- [x] depends on: #429 Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
This is a bare minimum port of the definitions of
Finset
/Multiset
/Fintype
. I am hoping that these are enough to port thefin_cases
tactic. (i.e. replacing the unfinished work in #346, which still had sorries in the corresponding material)Where possible I have started by copying and pasting the output from
mathlib3port
.