Idris2Doc : Data.List.Map

Data.List.Map

(source)

Definitions

recordListMap : Type->Type->Type
Totality: total
Visibility: public export
Constructor: 
MkListMap : Eqk=>List (k, v) ->ListMapkv

Projections:
.eq : ListMapkv->Eqk
.kvList : ListMapkv->List (k, v)

Hints:
Foldable (ListMapk)
Functor (ListMapk)
(Ordk, Semigroupv) =>Monoid (ListMapkv)
Semigroupv=>Semigroup (ListMapkv)
(Showk, Showv) =>Show (ListMapkv)
Traversable (ListMapk)
.eq : ListMapkv->Eqk
Totality: total
Visibility: public export
eq : ListMapkv->Eqk
Totality: total
Visibility: public export
.kvList : ListMapkv->List (k, v)
Totality: total
Visibility: public export
kvList : ListMapkv->List (k, v)
Totality: total
Visibility: public export
empty : Eqk=>ListMapkv
Totality: total
Visibility: export
lookup : k->ListMapkv->Maybev
Totality: total
Visibility: export
lookup' : ListMapkv->k->Maybev
Totality: total
Visibility: public export
insert : k->v->ListMapkv->ListMapkv
Totality: total
Visibility: export
insertWith : (v->v->v) ->k->v->ListMapkv->ListMapkv
  Inserts a key value pair into a map and merges duplicated values
with the given function.

Totality: total
Visibility: export
insert' : ListMapkv-> (k, v) ->ListMapkv
Totality: total
Visibility: public export
insertFrom : Foldablef=>f (k, v) ->ListMapkv->ListMapkv
Totality: total
Visibility: export
insertFrom' : Foldablef=>ListMapkv->f (k, v) ->ListMapkv
Totality: total
Visibility: public export
insertFromWith : Foldablef=> (v->v->v) ->f (k, v) ->ListMapkv->ListMapkv
  Inserts any foldable of a key value pair into a map and merges duplicated
values with the given function.

Totality: total
Visibility: export
singleton : Eqk=>k->v->ListMapkv
Totality: total
Visibility: export
updateExisting : (v->v) ->k->ListMapkv->ListMapkv
  Updates existing value, if it is present, and does nothing otherwise

The current implementation performs up to two traversals of the original map

Totality: total
Visibility: export
updateExisting' : ListMapkv-> (v->v) ->k->ListMapkv
Totality: total
Visibility: public export
fromList : Eqk=>List (k, v) ->ListMapkv
Totality: total
Visibility: public export
rawKeys : ListMapkv->Listk
  Returns the keys from the underlying list of key–value pairs
without removing duplicates or normalising the order.

Totality: total
Visibility: public export
rawValues : ListMapkv->Listv
  Returns the values from the underlying list of key–value pairs
in their original order, without any normalisation.

Totality: total
Visibility: public export
normalise : ListMapkv->ListMapkv
Totality: total
Visibility: export
keys : ListMapkv->Listk
  Gets the keys of the map.

Totality: total
Visibility: export
keySet : ListMapkv->ListSetk
Totality: total
Visibility: export
values : ListMapkv->Listv
  Gets the values of the map. Could contain duplicates.

Totality: total
Visibility: public export
mapWithKey : (k->a->b) ->ListMapka->ListMapkb
Totality: total
Visibility: export
mapWithKey' : ListMapka-> (k->a->b) ->ListMapkb
Totality: total
Visibility: export
mergeWith : (v->v->v) ->ListMapkv->ListMapkv->ListMapkv
  Merge two maps. When encountering duplicate keys, using a function to combine the values.
Uses the ordering of the first map given.

Totality: total
Visibility: export
merge : Semigroupv=>ListMapkv->ListMapkv->ListMapkv
  Merge two maps using the Semigroup (and by extension, Monoid) operation.
Uses mergeWith internally, so the ordering of the left map is kept.

Totality: total
Visibility: export
mergeLeft : ListMapkv->ListMapkv->ListMapkv
  Left-biased merge, also keeps the equality specified by the left map.

Totality: total
Visibility: export
toSortedMap : Ordk=>ListMapkv->SortedMapkv
Totality: total
Visibility: public export