Libraries.Data.IntMap

Definitions

data IntMap : Type -> Type

Totality: total
Visibility: export
Constructors:

Empty : IntMap v

M : (n : Nat) -> Tree n v -> IntMap v

Hints:

Functor IntMap

Semigroup v => Monoid (IntMap v)

Semigroup v => Semigroup (IntMap v)

empty : IntMap v

Totality: total
Visibility: export

lookup : Int -> IntMap v -> Maybe v

Totality: total
Visibility: export

insert : Int -> v -> IntMap v -> IntMap v

Totality: total
Visibility: export

singleton : Int -> v -> IntMap v

Totality: total
Visibility: export

insertFrom : List (Int, v) -> IntMap v -> IntMap v

Totality: total
Visibility: export

delete : Int -> IntMap v -> IntMap v

Totality: total
Visibility: export

fromList : List (Int, v) -> IntMap v

Totality: total
Visibility: export

toList : IntMap v -> List (Int, v)

Totality: total
Visibility: export

keys : IntMap v -> List Int

  Gets the Keys of the map.

Totality: total
Visibility: export

values : IntMap v -> List v

  Gets the values of the map. Could contain duplicates.

Totality: total
Visibility: export

mergeWith : (v -> v -> v) -> IntMap v -> IntMap v -> IntMap v

  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 : Semigroup v => IntMap v -> IntMap v -> IntMap v

  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 : IntMap v -> IntMap v -> IntMap v

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

Totality: total
Visibility: export