Idris2Doc : Data.Indexed.Add

Data.Indexed.Add

(source)
We can make any collection into an indexed collection by storing
pairs

Definitions

recordIndexed : (Type->Type) ->Type->Type->Type
Totality: total
Visibility: public export
Constructor: 
AddIndex : t (i, a) ->Indexedtia

Projection: 
.unIndex : Indexedtia->t (i, a)

Hints:
Filterablet=>Filterable (Indexedti)
Foldablet=>Foldable (Indexedti)
Functort=>Functor (Indexedti)
Filterablet=>IndFilterablei (Indexedti)
(Functort, Foldablet) =>IndFoldablei (Indexedti)
Functort=>IndFunctori (Indexedti)
Traversablet=>IndTraversablei (Indexedti)
Traversablet=>Traversable (Indexedti)
Witherablet=>Witherable (Indexedti)
.unIndex : Indexedtia->t (i, a)
Visibility: public export
unIndex : Indexedtia->t (i, a)
Visibility: public export