Idris2Doc : Data.SortedMap.Dependent

Data.SortedMap.Dependent

Definitions

dataSortedDMap : (k : Type) -> (k->Type) ->Type
Totality: total
Visibility: export
Constructors:
Empty : Ordk=>SortedDMapkv
M : {autoo : Ordk} -> (n : Nat) ->Treenkvo->SortedDMapkv

Hints:
Cast (SortedDMapk (constv)) (SortedMapkv)
Cast (SortedMapkv) (SortedDMapk (constv))
(DecEqk, Eq (vx)) =>Eq (SortedDMapkv)
DecEqk=>Ordk=>Semigroup (vx) =>Monoid (SortedDMapkv)
DecEqk=>Semigroup (vx) =>Semigroup (SortedDMapkv)
(Showk, Show (vx)) =>Show (SortedDMapkv)
empty : Ordk=>SortedDMapkv
Visibility: export
lookup : k->SortedDMapkv->Maybe (DPairk (\y=>vy))
Visibility: export
lookupPrecise : DecEqk=> (x : k) ->SortedDMapkv->Maybe (vx)
Visibility: export
insert : (x : k) ->vx->SortedDMapkv->SortedDMapkv
Visibility: export
singleton : Ordk=> (x : k) ->vx->SortedDMapkv
Visibility: export
insertFrom : Foldablef=>f (DPairk (\x=>vx)) ->SortedDMapkv->SortedDMapkv
Visibility: export
delete : k->SortedDMapkv->SortedDMapkv
Visibility: export
fromList : Ordk=>List (DPairk (\x=>vx)) ->SortedDMapkv
Visibility: export
toList : SortedDMapkv->List (DPairk (\x=>vx))
Visibility: export
keys : SortedDMapkv->Listk
  Gets the keys of the map.

Visibility: export
values : SortedDMapkv->List (DPairk (\x=>vx))
Visibility: export
map : (vx->wx) ->SortedDMapkv->SortedDMapkw
Visibility: export
foldl : (acc->DPairk (\x=>vx) ->acc) ->acc->SortedDMapkv->acc
Visibility: export
foldr : (DPairk (\x=>vx) ->acc->acc) ->acc->SortedDMapkv->acc
Visibility: export
foldlM : Monadm=> (acc->DPairk (\x=>vx) ->macc) ->acc->SortedDMapkv->macc
Visibility: export
foldMap : Monoidm=> ((x : k) ->vx->m) ->SortedDMapkv->m
Visibility: export
null : SortedDMapkv->Bool
Visibility: export
traverse : Applicativef=> (vx->f (wx)) ->SortedDMapkv->f (SortedDMapkw)
Visibility: export
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.

Visibility: export
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.

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

Visibility: export
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

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

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

Visibility: export
strictSubmap : DecEqk=>Eq (vx) =>SortedDMapkv->SortedDMapkv->Bool
Visibility: export