Data.SortedMap.Dependent

data SortedDMap : (k : Type) -> (k -> Type) -> Type

Totality: total
Constructors:

Empty : Ord k => SortedDMap k v
M : {auto o : Ord k} -> (n : Nat) -> Tree n k v o -> SortedDMap k v

delete : k -> SortedDMap k v -> SortedDMap k v

empty : Ord k => SortedDMap k v

foldMap : Monoid m => ((x : k) -> v x -> m) -> SortedDMap k v -> m

foldl : (acc -> DPair k (\x => v x) -> acc) -> acc -> SortedDMap k v -> acc

foldlM : Monad m => (acc -> DPair k (\x => v x) -> m acc) -> acc -> SortedDMap k v -> m acc

foldr : (DPair k (\x => v x) -> acc -> acc) -> acc -> SortedDMap k v -> acc

fromList : Ord k => List (DPair k (\x => v x)) -> SortedDMap k v

insert : (x : k) -> v x -> SortedDMap k v -> SortedDMap k v

insertFrom : Foldable f => f (DPair k (\x => v x)) -> SortedDMap k v -> SortedDMap k v

keys : SortedDMap k v -> List k

  Gets the keys of the map.

leftMost : SortedDMap k v -> Maybe (DPair k (\x => v x))

  Returns the leftmost (least) key and value

lookup : k -> SortedDMap k v -> Maybe (DPair k (\y => v y))

lookupBetween : k -> SortedDMap k v -> (Maybe (DPair k (\x => v x)), Maybe (DPair k (\x => v x)))

  looks up a key in map, returning the left and right closest values, so that
  k1 <= k < k2. If at the end of the beginning and/or end of the sorted map, returns
  nothing appropriately

lookupPrecise : DecEq k => (x : k) -> SortedDMap k v -> Maybe (v x)

map : (v x -> w x) -> SortedDMap k v -> SortedDMap k w

merge : DecEq k => Semigroup (v x) => SortedDMap k v -> SortedDMap k v -> SortedDMap k v

  Merge two maps using the Semigroup (and by extension, Monoid) operation.
  Uses mergeWith internally, so the ordering of the left map is kept.

mergeLeft : DecEq k => SortedDMap k v -> SortedDMap k v -> SortedDMap k v

  Left-biased merge, also keeps the ordering specified by the left map.

mergeWith : DecEq k => (v x -> v x -> v x) -> SortedDMap k v -> SortedDMap k v -> SortedDMap k v

  Merge two maps. When encountering duplicate keys, using a function to combine the values.
  Uses the ordering of the first map given.

null : SortedDMap k v -> Bool

rightMost : SortedDMap k v -> Maybe (DPair k (\x => v x))

  Returns the rightmost (greatest) key and value

singleton : Ord k => (x : k) -> v x -> SortedDMap k v

strictSubmap : DecEq k => Eq (v x) => SortedDMap k v -> SortedDMap k v -> Bool

toList : SortedDMap k v -> List (DPair k (\x => v x))

traverse : Applicative f => (v x -> f (w x)) -> SortedDMap k v -> f (SortedDMap k w)

values : SortedDMap k v -> List (DPair k (\x => v x))