Merge pull request #4772 from clayrat/patch-16
add SortedMap.singleton
commitf3cff2805998bdd6538d0998958c56d1c2ce1c7b
authorNiklas Larsson <metaniklas@gmail.com>
dateThu 7 Nov 2019, 15:17 (7 years ago)
parent103a454e6b19fb
libs/contrib/Data/SortedMap.idr+4
@@ -201,6 +201,10 @@ export
201201empty : Ord k => SortedMap k v
202202empty = Empty
203203
204+export
205+singleton : Ord k => k -> v -> SortedMap k v
206+singleton k v = M Z (Leaf k v)
207+
204208export
205209lookup : k -> SortedMap k v -> Maybe v
206210lookup _ Empty = Nothing