Idris2Doc : Data.SortedMap.Dependent

Data.SortedMap.Dependent

dataSortedDMap : (k : Type) -> (k -> Type) -> Type
Totality: total
Constructors:
Empty : Ordk => SortedDMapkv
M : {autoo : Ordk} -> (n : Nat) -> Treenkvo -> SortedDMapkv
delete : k -> SortedDMapkv -> SortedDMapkv
empty : Ordk => SortedDMapkv
foldMap : Monoidm => ((x : k) -> vx -> m) -> SortedDMapkv -> m
foldl : (acc -> DPairk (\x => vx) -> acc) -> acc -> SortedDMapkv -> acc
foldlM : Monadm => (acc -> DPairk (\x => vx) -> macc) -> acc -> SortedDMapkv -> macc
foldr : (DPairk (\x => vx) -> acc -> acc) -> acc -> SortedDMapkv -> acc
fromList : Ordk => List (DPairk (\x => vx)) -> SortedDMapkv
insert : (x : k) -> vx -> SortedDMapkv -> SortedDMapkv
insertFrom : Foldablef => f (DPairk (\x => vx)) -> SortedDMapkv -> SortedDMapkv
keys : SortedDMapkv -> Listk
  Gets the keys of the map.

leftMost : SortedDMapkv -> Maybe (DPairk (\x => vx))
  Returns the leftmost (least) key and value

lookup : k -> SortedDMapkv -> Maybe (DPairk (\y => vy))
lookupBetween : k -> SortedDMapkv -> (Maybe (DPairk (\x => vx)), Maybe (DPairk (\x => vx)))
  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 : DecEqk => (x : k) -> SortedDMapkv -> Maybe (vx)
map : (vx -> wx) -> SortedDMapkv -> SortedDMapkw
merge : DecEqk => Semigroup (vx) => SortedDMapkv -> SortedDMapkv -> SortedDMapkv
  Merge two maps using the Semigroup (and by extension, Monoid) operation.
Uses mergeWith internally, so the ordering of the left map is kept.

mergeLeft : DecEqk => SortedDMapkv -> SortedDMapkv -> SortedDMapkv
  Left-biased merge, also keeps the ordering specified by the left map.

mergeWith : DecEqk => (vx -> vx -> vx) -> SortedDMapkv -> SortedDMapkv -> SortedDMapkv
  Merge two maps. When encountering duplicate keys, using a function to combine the values.
Uses the ordering of the first map given.

null : SortedDMapkv -> Bool
rightMost : SortedDMapkv -> Maybe (DPairk (\x => vx))
  Returns the rightmost (greatest) key and value

singleton : Ordk => (x : k) -> vx -> SortedDMapkv
strictSubmap : DecEqk => Eq (vx) => SortedDMapkv -> SortedDMapkv -> Bool
toList : SortedDMapkv -> List (DPairk (\x => vx))
traverse : Applicativef => (vx -> f (wx)) -> SortedDMapkv -> f (SortedDMapkw)
values : SortedDMapkv -> List (DPairk (\x => vx))