Idris2Doc : Data.SortedMap.Extra

Data.SortedMap.Extra

(source)
Reexports
import public Syntax.IHateParens
Definitions
mapMaybe : Ord k => (a -> Maybe b) -> SortedMap k a -> SortedMap k b
  Totality: total
  Visibility: export
mapWithKey : Ord k => (k -> a -> b) -> SortedMap k a -> SortedMap k b
  Totality: total
  Visibility: export
mapWithKey' : Ord k => SortedMap k a -> (k -> a -> b) -> SortedMap k b
  Totality: total
  Visibility: public export
mapAsList : (f : (v -> w)) -> (m : SortedMap k v) -> (map f m) .asList = map (mapSnd f) (m .asList)
  Totality: total
  Visibility: export
mapSize : (f : (v -> w)) -> (m : SortedMap k v) -> (map f m) .size = m .size
  Totality: total
  Visibility: export
keySetSize : (m : SortedMap k v) -> (keySet m) .size = m .size
  Totality: total
  Visibility: export
keysThruAsList : (m : SortedMap k v) -> keys m = fst <$> m .asList
  Totality: total
  Visibility: export