Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(order/basic): Notation for order_dual #13798

Closed
wants to merge 30 commits into from
Closed

[Merged by Bors] - feat(order/basic): Notation for order_dual #13798

wants to merge 30 commits into from

Conversation

YaelDillies
Copy link
Collaborator

@YaelDillies YaelDillies commented Apr 29, 2022 •
edited
Loading

Define αᵒᵈ as notation for order_dual α and replace current uses.

Zulip poll

Open in Gitpod

@YaelDillies YaelDillies added awaiting-review The author would like community review of the PR awaiting-CI The author would like to see what CI has to say before doing more work. labels Apr 29, 2022
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Apr 30, 2022
@YaelDillies YaelDillies mentioned this pull request Apr 30, 2022
Merged
vihdzp
vihdzp reviewed Apr 30, 2022
View reviewed changes
Copy link
Collaborator

@vihdzp vihdzp left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I've highlighted everything I consider even slightly controversial. The rest of this huge PR is just changing the notation.

src/data/finset/lattice.lean Outdated Show resolved Hide resolved
src/data/set/intervals/basic.lean Outdated Show resolved Hide resolved
src/order/lattice.lean Outdated Show resolved Hide resolved
src/topology/algebra/order/basic.lean Outdated Show resolved Hide resolved
src/order/omega_complete_partial_order.lean Outdated Show resolved Hide resolved
@YaelDillies
Copy link
Collaborator Author

Reverted them all and singled them out to #13839.

eric-wieser
eric-wieser reviewed May 2, 2022
View reviewed changes
src/order/circular.lean Outdated Show resolved Hide resolved
eric-wieser
eric-wieser reviewed May 2, 2022
View reviewed changes
src/order/basic.lean Outdated Show resolved Hide resolved
@eric-wieser eric-wieser added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels May 2, 2022
@YaelDillies YaelDillies added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels May 2, 2022
@kim-em kim-em added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label May 2, 2022
@kim-em kim-em removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label May 2, 2022
@YaelDillies YaelDillies mentioned this pull request May 4, 2022
Closed
1 task
jcommelin
jcommelin approved these changes May 4, 2022
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks 🎉

bors merge

@leanprover-community-bot-assistant leanprover-community-bot-assistant added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels May 4, 2022
bors bot pushed a commit that referenced this pull request May 4, 2022
@YaelDillies
feat(order/basic): Notation for order_dual (#13798)
a057441 
Define `αᵒᵈ` as notation for `order_dual α` and replace current uses.

[Zulip poll](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Notation.20for.20order_dual/near/280629129)
@bors
Copy link

bors bot commented May 4, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(order/basic): Notation for order_dual [Merged by Bors] - feat(order/basic): Notation for order_dual May 4, 2022
@bors bors bot closed this May 4, 2022
@bors bors bot deleted the order_dual_notation branch May 4, 2022 13:13
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

@vihdzp vihdzp vihdzp left review comments

@eric-wieser eric-wieser eric-wieser left review comments

@jcommelin jcommelin jcommelin approved these changes

Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
6 participants
@YaelDillies @eric-wieser @jcommelin @vihdzp @kim-em @leanprover-community-bot-assistant