on master help sign in
Merge pull request #4772 from clayrat/patch-16
f3cff28Niklas Larsson
libs/contrib/Data/SortedMap.idr+4
@@ -201,6 +201,10 @@ export
201empty : Ord k => SortedMap k v
201empty : Ord k => SortedMap k v
202empty = Empty
202empty = Empty
203
203
204+export
205+singleton : Ord k => k -> v -> SortedMap k v
206+singleton k v = M Z (Leaf k v)
207+
204export
208export
205lookup : k -> SortedMap k v -> Maybe v
209lookup : k -> SortedMap k v -> Maybe v
206lookup _ Empty = Nothing
210lookup _ Empty = Nothing