-
Notifications
You must be signed in to change notification settings - Fork 297
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(data/finset): provide the coercion finset α → Type*
#7575
Conversation
Can you add |
There's the obvious fintype instance which should be added on such a type. |
d788ce1
to
afd5bf7
Compare
It (finally!) builds on my machine now. Let's see what the linter thinks. |
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.
Looks good to me, but I think another pair of eyes on it would be good.
bors merge |
Merge conflict. |
The conflict was just two additions in the same place, easy to fix. Currently recompiling to see if anything breaks. |
This has been bugging me for a while and I have no good explanantion why it was missing. I'll let the CI run for a bit to see if the linters can explain why. TODO: get rid of the (obvious?) instances of the old pattern `(((s : finset α) : set α) : Type*)`
I definitely missed a number of them. I think I'll leave that for other cleanup commits.
bb94b2b
to
cd97421
Compare
Feel free to merge (again) if this builds! |
✌️ Vierkantor can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
There doesn't seem to be a good reason that `finset` doesn't have a `coe_to_sort` like `set` does. Before the change in this PR, we had to suffer the inconvenience of writing `(↑s : set _)` whenever we want the subtype of all elements of `s`. Now you can just write `s`. I removed the obvious instances of the `((↑s : set _) : Type*)` pattern, although it definitely remains in some places. I'd rather do those in separate PRs since it does not really do any harm except for being annoying to type. There are also some parts of the API (`polynomial.root_set` stands out to me) that could be designed around the use of `finset`s rather than `set`s that are later proved to be finite, which I again would like to declare out of scope.
Build failed (retrying...): |
There doesn't seem to be a good reason that `finset` doesn't have a `coe_to_sort` like `set` does. Before the change in this PR, we had to suffer the inconvenience of writing `(↑s : set _)` whenever we want the subtype of all elements of `s`. Now you can just write `s`. I removed the obvious instances of the `((↑s : set _) : Type*)` pattern, although it definitely remains in some places. I'd rather do those in separate PRs since it does not really do any harm except for being annoying to type. There are also some parts of the API (`polynomial.root_set` stands out to me) that could be designed around the use of `finset`s rather than `set`s that are later proved to be finite, which I again would like to declare out of scope.
Build failed (retrying...): |
There doesn't seem to be a good reason that `finset` doesn't have a `coe_to_sort` like `set` does. Before the change in this PR, we had to suffer the inconvenience of writing `(↑s : set _)` whenever we want the subtype of all elements of `s`. Now you can just write `s`. I removed the obvious instances of the `((↑s : set _) : Type*)` pattern, although it definitely remains in some places. I'd rather do those in separate PRs since it does not really do any harm except for being annoying to type. There are also some parts of the API (`polynomial.root_set` stands out to me) that could be designed around the use of `finset`s rather than `set`s that are later proved to be finite, which I again would like to declare out of scope.
Pull request successfully merged into master. Build succeeded: |
finset α → Type*
finset α → Type*
There doesn't seem to be a good reason that
finset
doesn't have acoe_to_sort
likeset
does. Before the change in this PR, we had to suffer the inconvenience of writing(↑s : set _)
whenever we want the subtype of all elements ofs
. Now you can just writes
.I removed the obvious instances of the
((↑s : set _) : Type*)
pattern, although it definitely remains in some places. I'd rather do those in separate PRs since it does not really do any harm except for being annoying to type. There are also some parts of the API (polynomial.root_set
stands out to me) that could be designed around the use offinset
s rather thanset
s that are later proved to be finite, which I again would like to declare out of scope.