Skip to content

Commit

Permalink
[ base ] Data.SortedSet.leftMost and .rightMost (#3260)
Browse files Browse the repository at this point in the history
* [ base ] Data.SortedSet.leftMost and .rightMost

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

* contributors

---------

Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
  • Loading branch information
MithicSpirit and gallais committed Jun 5, 2024
1 parent 40d4cd8 commit f83ad9c
Show file tree
Hide file tree
Showing 3 changed files with 13 additions and 0 deletions.
2 changes: 2 additions & 0 deletions CHANGELOG_NEXT.md
Original file line number Diff line number Diff line change
Expand Up @@ -139,6 +139,8 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO

* Removed need for the runtime value of the implicit argument in `succNotLTEpred`.

* Implemented `leftMost` and `rightMost` for `SortedSet`.

* Added `funExt0` and `funExt1`, functions analogous to `funExt` but for functions
with quantities 0 and 1 respectively.

Expand Down
1 change: 1 addition & 0 deletions CONTRIBUTORS
Original file line number Diff line number Diff line change
Expand Up @@ -57,6 +57,7 @@ Nicolas Biri
Niklas Larsson
Ohad Kammar
Peter Hajdu
Ricardo Prado Cunha
Robert Walter
rhiannon morris
Rodrigo Oliveira
Expand Down
10 changes: 10 additions & 0 deletions libs/base/Data/SortedSet.idr
Original file line number Diff line number Diff line change
Expand Up @@ -62,6 +62,16 @@ export
intersection : (x, y : SortedSet k) -> SortedSet k
intersection x y = difference x (difference x y)

||| Returns the leftmost (least) value
export
leftMost : SortedSet k -> Maybe k
leftMost (SetWrapper m) = fst <$> leftMost m

||| Returns the rightmost (greatest) value
export
rightMost : SortedSet k -> Maybe k
rightMost (SetWrapper m) = fst <$> rightMost m

export
Ord k => Semigroup (SortedSet k) where
(<+>) = union
Expand Down

0 comments on commit f83ad9c

Please sign in to comment.