add SortedMap.singleton
commite6b19fb42dfa746097ca373a0b7745a97aae89f5
authorAlex Gryzlov <skyrodent@gmail.com>
dateFri 25 Oct 2019, 23:38 (7 years ago)
parent095fb31
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