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/rel_iso): a new definition of order_iso, using preorder instances #3838
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.
Thank you for the PR, it fixes an irritation I've been having for a while.
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. Anyone with more experience in the order
part of the library who wants to comment?
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.
It's been a day so Let's Get This Merged.
bors r+
…stances (#3838) defines (new) `order_embedding` and `order_iso`, which map both < and <= replaces existing `rel_embedding` and `rel_iso` instances preserving < or <= with the new abbreviations
Pull request successfully merged into master. Build succeeded: |
…stances (#3838) defines (new) `order_embedding` and `order_iso`, which map both < and <= replaces existing `rel_embedding` and `rel_iso` instances preserving < or <= with the new abbreviations
defines (new)
order_embedding
andorder_iso
, which map both < and <=replaces existing
rel_embedding
andrel_iso
instances preserving < or <= with the new abbreviations