Skip to content
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.

Sign up for GitHub

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

Jump to bottom

feat(order/directed): Add codirected_order class and associated instances. #7980

Closed
wants to merge 3 commits into from
Closed

feat(order/directed): Add codirected_order class and associated instances. #7980

wants to merge 3 commits into from

Conversation

adamtopaz
Copy link
Collaborator

@adamtopaz adamtopaz commented Jun 17, 2021 •
edited

The added instances break the original proof of multiset.ndunion_le, hence the modified proof in this PR. See related zulip discussion here

Open in Gitpod

@adamtopaz adamtopaz added awaiting-review The author would like community review of the PR WIP Work in progress and removed awaiting-review The author would like community review of the PR labels Jun 17, 2021
@eric-wieser
Copy link
Member

I tried this in #7163 and ran into possibly similar problems

@adamtopaz
Copy link
Collaborator Author

To be honest, this seems to require much more work and time than I expected with very little payoff. I'll mark as please-adopt, in case anyone is brave enough and has the time.

@adamtopaz adamtopaz added the please-adopt This PR/issue may have been abandoned by the original contributor. You are welcome to take it over. label Jun 18, 2021
@YaelDillies YaelDillies mentioned this pull request Sep 14, 2021
Closed
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Jan 13, 2022
@YaelDillies
Copy link
Collaborator

For obscure reasons, inserting directed_order severely breaks random stuff downstream. I've had better luck with my relation class is_directed, so this PR is now irrelevant. See #11238

As future work, we might want to add directed_order/codirected_order as shorthands for is_directed α (≤)/is_directed α (swap (≤)).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
merge-conflict Please `git merge origin/master` then a bot will remove this label. please-adopt This PR/issue may have been abandoned by the original contributor. You are welcome to take it over. WIP Work in progress
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@adamtopaz @eric-wieser @YaelDillies @leanprover-community-bot-assistant