From f83ad9ce980cda9420f3e00a21f62ac6f5b837f8 Mon Sep 17 00:00:00 2001 From: MithicSpirit Date: Wed, 5 Jun 2024 07:00:57 -0400 Subject: [PATCH] [ base ] Data.SortedSet.leftMost and .rightMost (#3260) * [ 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 --- CHANGELOG_NEXT.md | 2 ++ CONTRIBUTORS | 1 + libs/base/Data/SortedSet.idr | 10 ++++++++++ 3 files changed, 13 insertions(+) diff --git a/CHANGELOG_NEXT.md b/CHANGELOG_NEXT.md index 0738350d68..aadb887eb5 100644 --- a/CHANGELOG_NEXT.md +++ b/CHANGELOG_NEXT.md @@ -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. diff --git a/CONTRIBUTORS b/CONTRIBUTORS index 677ff6c62c..4e2d89f902 100644 --- a/CONTRIBUTORS +++ b/CONTRIBUTORS @@ -57,6 +57,7 @@ Nicolas Biri Niklas Larsson Ohad Kammar Peter Hajdu +Ricardo Prado Cunha Robert Walter rhiannon morris Rodrigo Oliveira diff --git a/libs/base/Data/SortedSet.idr b/libs/base/Data/SortedSet.idr index d954be1410..25611af806 100644 --- a/libs/base/Data/SortedSet.idr +++ b/libs/base/Data/SortedSet.idr @@ -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