[Merged by Bors] - chore(order/galois_connection): ask for the correct instances #7594
Conversation
YaelDillies
added
awaiting-review
|
can you nick my changes from #7592 so that it doesn't become a merge conflict? i'll close the PR after |
|
|
||
| lemma is_lub_u {b : β} : is_lub { a | l a ≤ b } (u b) := | ||
| ⟨assume b, gc.le_u, assume b h, h $ gc.l_u_le _⟩ | ||
| ⟨λ b, gc.le_u, λ b h, h $ gc.l_u_le _⟩ | ||
|
|
||
| end | ||
|
|
||
| section partial_order |
There was a problem hiding this comment.
is it maybe worth combining both partial_order sections and just specifiying the parameters in the signature? it looks quite clunky (but maybe only in the diff view, I read it in the normal view and it seemed better)
There was a problem hiding this comment.
Yeah, I don't know. I only moved one lemma above two others. But also each section is only used for two lemmas.
There was a problem hiding this comment.
Otherwise LGTM. Feel free to merge after fixing this and incorporating the changes mentioned by @ericrbg if you wish.
bors d+
|
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
delegated
Done! You missed the most obvious " if |
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
|
bors r+ |
|
bors merge |
|
Bors doesn't seem to have picked up the command. Is it doing anything? How can I check? |
|
The Bors queue is here, indeed, it doesn't seem to have picked it up |
|
bors merge |
|
There was an issue with bors itself: bors-ng/bors-ng#1246 |
github-actions
bot
added
the
ready-to-merge
replace partial_order by preorder where it can and general tidy up of this old style file
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
replace partial_order by preorder where it can and general tidy up of this old style file