Data.Fin.Map

Specialised map from `Fin`s to any type.
Isomorphic to a vector of appropriate size of maybe's of appropriate type.

This should be a replacement for `SortedMap (Fin n) v` working better at least in elaborator scripts.

Definitions

data FinMap : Nat -> Type -> Type

Totality: total
Visibility: export
Constructor: 

MkFM : Vect n (Maybe v) -> FinMap n v

Hints:

Eq v => Eq (FinMap n v)

Foldable (FinMap n)

Functor (FinMap n)

Interpolation v => Interpolation (Fin n) => Interpolation (FinMap n v)

Semigroup v => Monoid (FinMap n v)

Semigroup v => Semigroup (FinMap n v)

Traversable (FinMap n)

Zippable (FinMap n)

empty : FinMap n v

Totality: total
Visibility: export

lookup : Fin n -> FinMap n v -> Maybe v

Totality: total
Visibility: export

lookup' : FinMap n v -> Fin n -> Maybe v

Totality: total
Visibility: export

insert : Fin n -> v -> FinMap n v -> FinMap n v

Totality: total
Visibility: export

insertWith : (v -> v -> v) -> Fin n -> v -> FinMap n v -> FinMap n v

Totality: total
Visibility: export

insert' : FinMap n v -> (Fin n, v) -> FinMap n v

Totality: total
Visibility: public export

singleton : Fin n -> v -> FinMap n v

Totality: total
Visibility: export

insertFrom : Foldable f => f (Fin n, v) -> FinMap n v -> FinMap n v

Totality: total
Visibility: export

insertFrom' : Foldable f => FinMap n v -> f (Fin n, v) -> FinMap n v

Totality: total
Visibility: export

insertFromWith : Foldable f => (v -> v -> v) -> f (Fin n, v) -> FinMap n v -> FinMap n v

Totality: total
Visibility: export

delete : Fin n -> FinMap n v -> FinMap n v

Totality: total
Visibility: export

delete' : FinMap n v -> Fin n -> FinMap n v

Totality: total
Visibility: export

update : (Maybe v -> Maybe v) -> Fin n -> FinMap n v -> FinMap n v

Totality: total
Visibility: export

update' : FinMap n v -> (Maybe v -> Maybe v) -> Fin n -> FinMap n v

Totality: total
Visibility: public export

updateExisting : (v -> v) -> Fin n -> FinMap n v -> FinMap n v

Totality: total
Visibility: export

updateExisting' : FinMap n v -> (v -> v) -> Fin n -> FinMap n v

Totality: total
Visibility: public export

fromFoldable : Foldable f => f (Fin n, v) -> FinMap n v

Totality: total
Visibility: export

fromFoldableWith : Foldable f => (v -> v -> v) -> f (Fin n, v) -> FinMap n v

Totality: total
Visibility: export

fromList : List (Fin n, v) -> FinMap n v

Totality: total
Visibility: export

fromListWith : (v -> v -> v) -> List (Fin n, v) -> FinMap n v

Totality: total
Visibility: export

iList : Vect n a -> List (Fin n, a)

Totality: total
Visibility: export

kvList : FinMap n v -> List (Fin n, v)

Totality: total
Visibility: export

.asKVList : FinMap n v -> List (Fin n, v)

Totality: total
Visibility: public export

keys : FinMap n v -> List (Fin n)

Totality: total
Visibility: export

values : FinMap n v -> List v

Totality: total
Visibility: export

mapWithKey : (Fin n -> v -> w) -> FinMap n v -> FinMap n w

Totality: total
Visibility: export

mapWithKey' : FinMap n v -> (Fin n -> v -> w) -> FinMap n w

Totality: total
Visibility: export

traverseWithKey : Applicative m => (Fin n -> v -> m w) -> FinMap n v -> m (FinMap n w)

Totality: total
Visibility: export

forWithKey : Applicative m => FinMap n v -> (Fin n -> v -> m w) -> m (FinMap n w)

Totality: total
Visibility: public export

mergeWith : (v -> v -> v) -> FinMap n v -> FinMap n v -> FinMap n v

  Merge two maps, when encountering duplicate keys, uses a function to combine the values.

Totality: total
Visibility: export

merge : Semigroup v => FinMap n v -> FinMap n v -> FinMap n v

Totality: total
Visibility: public export

mergeLeft : FinMap n v -> FinMap n v -> FinMap n v

Totality: total
Visibility: public export

leftMost : FinMap n v -> Maybe (Fin n, v)

Totality: total
Visibility: export

rightMost : FinMap n v -> Maybe (Fin n, v)

Totality: total
Visibility: export

size : FinMap n v -> Nat

Totality: total
Visibility: public export

.size : FinMap n v -> Nat

Totality: total
Visibility: public export

.asKVVect : (fs : FinMap n v) -> Vect (fs .size) (Fin n, v)

Totality: total
Visibility: public export

fromSortedMap : SortedMap (Fin n) v -> FinMap n v

Totality: total
Visibility: export

weakenToSuper : FinMap (finToNat i) v -> FinMap n v

Totality: total
Visibility: export