Data.AssocList.Indexed

Definitions

record AssocList : Nat -> Type -> Type

Totality: total
Visibility: export
Constructor: 

AL : Rep k e -> AssocList k e

Projection: 

.ps : AssocList k e -> Rep k e

Hints:

Eq e => Eq (AssocList k e)

Foldable (AssocList k)

Functor (AssocList k)

Show e => Show (AssocList k e)

Traversable (AssocList k)

weakenAL : AssocList k e -> AssocList (S k) e

Totality: total
Visibility: export

weakenALN : (0 m : Nat) -> AssocList k e -> AssocList (k + m) e

Totality: total
Visibility: export

empty : AssocList k e

Totality: total
Visibility: export

singleton : Fin k -> e -> AssocList k e

Totality: total
Visibility: export

pairs : AssocList k e -> List (Fin k, e)

Totality: total
Visibility: export

mapKV : (Fin k -> e -> b) -> AssocList k e -> AssocList k b

Totality: total
Visibility: export

foldlKV : (Fin k -> acc -> e -> acc) -> acc -> AssocList k e -> acc

Totality: total
Visibility: export

traverseKV : Applicative f => ((Fin k, e) -> f b) -> AssocList k e -> f (AssocList k b)

Totality: total
Visibility: public export

lookup : Fin k -> AssocList k e -> Maybe e

  Lookup a key in an assoc list.

Totality: total
Visibility: export

hasKey : AssocList k e -> Fin k -> Bool

  Checks if an `AssocList` has an entry for the given key.

Totality: total
Visibility: export

nonEmpty : AssocList k e -> Bool

Totality: total
Visibility: export

isEmpty : AssocList k e -> Bool

Totality: total
Visibility: export

keys : AssocList k e -> List (Fin k)

  Extracts the keys from the assoc list.

Totality: total
Visibility: export

values : AssocList k e -> List e

  Extracts the values from the assoc list.

Totality: total
Visibility: export

length : AssocList k e -> Nat

Totality: total
Visibility: export

insert : Fin k -> e -> AssocList k e -> AssocList k e

  Inserts a new key / value pair into an assoc list.
  
  Note: If the given key `k` is already present in the assoc list,
  its associated value will be replaced with the new value.

Totality: total
Visibility: export

insertWith : (e -> e -> e) -> Fin k -> e -> AssocList k e -> AssocList k e

  Like `insert` but in case `k` is already present in the assoc
  list, the `v` will be cobine with the old value via function `f`.

Totality: total
Visibility: export

fromList : List (Fin k, e) -> AssocList k e

Totality: total
Visibility: export

delete : Fin k -> AssocList k e -> AssocList k e

  Tries to remove the entry with the given key from the
  assoc list. The key index of the result will be equal to
  or greater than `m`.

Totality: total
Visibility: export

mapMaybe : (e -> Maybe b) -> AssocList k e -> AssocList k b

  Applies the given function to all values, keeping only the
  `Just` results.

Totality: total
Visibility: export

mapMaybeK : (Fin k -> e -> Maybe b) -> AssocList k e -> AssocList k b

  Applies the given function to all key / value pairs, keeping only the
  `Just` results.

Totality: total
Visibility: export

update : Fin k -> (e -> e) -> AssocList k e -> AssocList k e

  Updates the value at the given position by applying the given function.

Totality: total
Visibility: export

updateA : Applicative f => Fin k -> (e -> f e) -> AssocList k e -> f (AssocList k e)

  Updates the value at the given position by applying the given effectful
  computation.

Totality: total
Visibility: export

union : AssocList k e -> AssocList k e -> AssocList k e

  Computes the union of two assoc lists.
  
  In case of identical keys, the value of the second list
  is dropped. Use `unionWith` for better control over handling
  duplicate entries.

Totality: total
Visibility: export

unionMap : (e -> e -> b) -> (e -> b) -> AssocList k e -> AssocList k e -> AssocList k b

  Like `union` but in case of identical keys appearing in
  both lists, the associated values are combined using
  function `f`. Otherwise, values are converted with `g`.

Totality: total
Visibility: export

unionWith : (e -> e -> e) -> AssocList k e -> AssocList k e -> AssocList k e

  Like `union` but in case of identical keys appearing in
  both lists, the associated values are combined using
  function `f`.

Totality: total
Visibility: export

intersectWith : (e -> e -> b) -> AssocList k e -> AssocList k e -> AssocList k b

  Computes the intersection of two assoc lists, keeping
  only entries appearing in both lists. Values of the two
  lists are combine using function `f`.

Totality: total
Visibility: export

intersect : AssocList k e -> AssocList k e -> AssocList k e

  Computes the intersection of two assoc lists, keeping
  only entries appearing in both lists. Only the values of
  the first list are being kept.

Totality: total
Visibility: export

filterLin : (Fin k -> F1 s Bool) -> AssocList k e -> F1 s (AssocList k e)

  Filter an assoc list via a linear function.

Totality: total
Visibility: export

minBy : Ord b => (a -> b) -> AssocList k a -> Maybe (Fin k, a)

  Using a comparator, find the minimal value and its
  index in an assoc list.

Totality: total
Visibility: export