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

[ base ] Data.SortedSet.leftMost and .rightMost #3260

Merged
merged 3 commits into from
Jun 5, 2024

Conversation

MithicSpirit
Copy link
Contributor

Description

Implement leftMost and rightMost for SortedSet in terms of the
functions with the same name in Data.SortedMap.

Should this change go in the CHANGELOG?

  • If this is a fix, user-facing change, a compiler change, or a new paper
    implementation, I have updated CHANGELOG_NEXT.md (and potentially also
    CONTRIBUTORS.md).

Implement `leftMost` and `rightMost` for `SortedSet` in terms of the
functions with the same name in `Data.SortedMap`.
@MithicSpirit
Copy link
Contributor Author

MithicSpirit commented Apr 18, 2024

Now that I think about this again, it might be better to call these minimum
and maximum since they correspond to the actual value that is returned. This
makes it more in-line with Data.List (which is missing maximum; working on
that now) rather than Data.SortedMap, which I think is preferable since the
use case of sets is closer to that of lists than that of maps. Please let me
know if you would like this change.

@gallais gallais merged commit f83ad9c into idris-lang:main Jun 5, 2024
3 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants