idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-24 06:52:19 +03:00
Code Issues Projects Releases Wiki Activity

[ new ] retrieving value associated with the minimal key from a SortedMap

Browse Source
This commit is contained in:
Justus Matthiesen 2023-02-06 17:15:35 +00:00 committed by G. Allais
parent 9bdc875b79
commit f2dfeb39cd
1 changed files with 9 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
src/Libraries/Data/SortedMap.idr
View File

@ -324,6 +324,15 @@ adjust k f m =
Nothing => m Nothing => m
Just v => insert k (f v) m Just v => insert k (f v) m
treeMin : Tree n k v o -> (k, v)
treeMin (Leaf k v) = (k, v)
treeMin (Branch2 t _ _) = treeMin t
treeMin (Branch3 t _ _ _ _) = treeMin t
export
min : SortedMap k v -> Maybe (k, v)
min Empty = Nothing
min (M _ t) = Just (treeMin t)
export export
(Show k, Show v) => Show (SortedMap k v) where (Show k, Show v) => Show (SortedMap k v) where
show m = "fromList " ++ (show $ SortedMap.toList m) show m = "fromList " ++ (show $ SortedMap.toList m)