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(order/locally_finite): introduce locally finite orders #9464
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.
Thanks!
Thanks 🎉 If CI passes, please remove the label bors d+ |
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
The new typeclass `locally_finite_order` homogeneizes treatment of intervals as `finset`s and `multiset`s. `finset.Ico` is now available for all locally finite orders (instead of being ℕ-specialized), rendering `finset.Ico_ℤ` and `pnat.Ico` useless. This PR also introduces the long-awaited `finset.Icc`, `finset.Ioc`, `finset.Ioo`, and `finset.Ici`, `finset.Ioi` (for `order_top`s) and `finset.Iic`, `finset.Iio` (for `order_bot`s), and the `multiset` variations thereof.
Pull request successfully merged into master. Build succeeded: |
The new typeclass
locally_finite_order
homogeneizes treatment of intervals asfinset
s andmultiset
s.finset.Ico
is now available for all locally finite orders (instead of being ℕ-specialized), renderingfinset.Ico_ℤ
andpnat.Ico
useless.This PR also introduces the long-awaited
finset.Icc
,finset.Ioc
,finset.Ioo
, andfinset.Ici
,finset.Ioi
(fororder_top
s) andfinset.Iic
,finset.Iio
(fororder_bot
s), and themultiset
variations thereof.I haven't redefined
finset.Ico
andmultiset.Ico
in this PR to avoid needing to change all the API. #7987 will take care offinset.Ico
and another PR will follow formultiset.Ico
.Another PR (reviving the branch fin_range) about intervals as ordered lists will hopefully follow. This is strictly less general than what we have here as many
locally_finite_order
s are nonlinear.