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/category/omega-complete): omega-complete partial orders form a complete category #4397
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.
I'm guessing you didn't mean to remove the simps
in the merge.
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
this looks good to me. From this point @b-mehta, how much is missing to have a CCC instance? |
From here I think the things you did in the original PR would work fine, I only intended this as a more general way of doing the binary product and terminal stuff you had! |
Super! Thank you so much! If Scott is happy with this, I am too! |
Sorry about the delay! bors merge |
Build failed (retrying...): |
Build failed: |
bors r+ |
Pull request successfully merged into master. Build succeeded: |
as discussed in #4348.