-
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] - chore: Remove order dependencies to Data.Fin.Basic
#13005
Conversation
Move all the declarations using the mathlib order hierarchy to a new file `Order.Fin`. There were a bunch of order embeddings in `Data.Fin.Basic`, so I kept an embedding version of them around and renamed the order embedding version.
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.
Should we add an assert_not_exists
statement in Data/Fin/Basic?
There's no meaningul |
Fair enough. |
bors r+ |
Move all the declarations using the mathlib order hierarchy to a new file `Order.Fin`. There were a bunch of order embeddings in `Data.Fin.Basic`, so I kept an embedding version of them around and renamed the order embedding version.
Pull request successfully merged into master. Build succeeded: |
Data.Fin.Basic
Data.Fin.Basic
Move all the declarations using the mathlib order hierarchy to a new file `Order.Fin`. There were a bunch of order embeddings in `Data.Fin.Basic`, so I kept an embedding version of them around and renamed the order embedding version.
This was removed in #13005.
This was removed in #13005.
Move all the declarations using the mathlib order hierarchy to a new file `Order.Fin`. There were a bunch of order embeddings in `Data.Fin.Basic`, so I kept an embedding version of them around and renamed the order embedding version.
This was removed in #13005.
Move all the declarations using the mathlib order hierarchy to a new file `Order.Fin`. There were a bunch of order embeddings in `Data.Fin.Basic`, so I kept an embedding version of them around and renamed the order embedding version.
Move all the declarations using the mathlib order hierarchy to a new file
Order.Fin
. There were a bunch of order embeddings inData.Fin.Basic
, so I kept an embedding version of them around and renamed the order embedding version.