Data.Indexed.AddDep

We can make any collection into an dependently indexed collection
by storing dependent pairs.

Definitions

record DepIndexed : (Type -> Type) -> (i : Type) -> (i -> Type) -> Type

Totality: total
Visibility: public export
Constructor: 

AddDepIndex : t (DPair i a) -> DepIndexed t i a

Projection: 

.unDepIndex : DepIndexed t i a -> t (DPair i a)

Hints:

Filterable t => DepFilterable i (DepIndexed t i)

Foldable t => DepFoldable i (DepIndexed t i)

Functor t => DepFunctor i (DepIndexed t i)

Traversable t => DepTraversable i (DepIndexed t i)

.unDepIndex : DepIndexed t i a -> t (DPair i a)

Visibility: public export

unDepIndex : DepIndexed t i a -> t (DPair i a)

Visibility: public export