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.

Definitions

data AtIndex : Fin n -> Vect n type -> type -> Type

Totality: total
Visibility: public export
Constructors:

Here : AtIndex FZ (x :: xs) x

There : AtIndex rest xs x -> AtIndex (FS rest) (y :: xs) x

elemDiffers : (y = x -> Void) -> AtIndex FZ (y :: xs) x -> Void

Totality: total
Visibility: public export

elemNotInRest : (AtIndex z xs x -> Void) -> AtIndex (FS z) (y :: xs) x -> Void

Totality: total
Visibility: public export

index : DecEq type => (idx : Fin n) -> (x : type) -> (xs : Vect n type) -> Dec (AtIndex idx xs x)

  Is the element at the given index?
  

Totality: total
Visibility: public export

elemNotInRest : (DPair type (AtIndex x xs) -> Void) -> DPair type (AtIndex (FS x) (y :: xs)) -> Void

Totality: total
Visibility: public export

index : DecEq type => (idx : Fin n) -> (xs : Vect n type) -> Dec (DPair type (AtIndex idx xs))

  What is the element at the given index?
  

Totality: total
Visibility: public export