Idris2Doc : Data.Vect.AtIndex

Data.Vect.AtIndex

Indexing Vectors.

`Elem` proofs give existential quantification that a given element
*is* in the list, but not where in the list it is!  Here we give a
predicate that presents proof that a given index of a vector,
given by a `Fin` instance, will return a certain element.

Two decidable decision procedures are presented:

1. Check that a given index points to the provided element in the
   presented vector.

2. Find the element at the given index in the presented vector.
dataAtIndex : Finn -> Vectntype -> type -> Type
Totality: total
Constructors:
Here : AtIndexFZ (x::xs) x
There : AtIndexrestxsx -> AtIndex (FSrest) (y::xs) x