idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-28 02:23:44 +03:00
Code Issues Projects Releases Wiki Activity

[ new ] popping key-value pair from a SortedMap

Browse Source
This commit is contained in:
Justus Matthiesen 2023-02-06 17:17:01 +00:00 committed by G. Allais
parent 5f7ad73a35
commit 692e389bb8
1 changed files with 7 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -333,6 +333,13 @@ export
min : SortedMap k v -> Maybe (k, v)
min Empty = Nothing
min (M _ t) = Just (treeMin t)
export
pop : SortedMap k v -> Maybe ((k, v), SortedMap k v)
pop m = do
(k, v) <- min m
pure ((k, v), delete k m)
export
(Show k, Show v) => Show (SortedMap k v) where
show m = "fromList " ++ (show $ SortedMap.toList m)