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.
```

## 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