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.

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

Added IsOrderFilter #707

Merged
merged 6 commits into from
Nov 27, 2024
Merged

Added IsOrderFilter #707

merged 6 commits into from
Nov 27, 2024

Conversation

zljlzljlz
Copy link
Contributor

#522 - returns true if the specified subset is upwards closed, false if not, based on IsOrderIdeal.

@james-d-mitchell james-d-mitchell added the new-feature A label for new features. label Oct 19, 2024
@mtorpey mtorpey self-requested a review November 6, 2024 16:10
@mtorpey
Copy link
Collaborator

mtorpey commented Nov 6, 2024

I took a look at this and offered @zljlzljlz some pointers. She made a lot of progress, which should hopefully be pushed soon.

@james-d-mitchell
Copy link
Member

Thanks both, I look forward to seeing this when pushed 👍

@mtorpey
Copy link
Collaborator

mtorpey commented Nov 20, 2024

It looks like doc/title.xml was added to the repo accidentally. Could you remove this?

Otherwise, this is looking good – I'd recommend merging after that change.

@james-d-mitchell
Copy link
Member

Agreed I'll be happy to merge when the title.xml file is removed. Thanks @zljlzljlz !

Copy link
Collaborator

@mtorpey mtorpey left a comment

Choose a reason for hiding this comment

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

Great

@mtorpey mtorpey merged commit 8062ca7 into digraphs:main Nov 27, 2024
25 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
new-feature A label for new features.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants