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

dataAtIndex : Finn->Vectntype->type->Type
Totality: total
Visibility: public export
Constructors:
Here : AtIndexFZ (x::xs) x
There : AtIndexrestxsx->AtIndex (FSrest) (y::xs) x
elemDiffers : (y=x->Void) ->AtIndexFZ (y::xs) x->Void
Totality: total
Visibility: public export
elemNotInRest : (AtIndexzxsx->Void) ->AtIndex (FSz) (y::xs) x->Void
Totality: total
Visibility: public export
index : DecEqtype=> (idx : Finn) -> (x : type) -> (xs : Vectntype) ->Dec (AtIndexidxxsx)
  Is the element at the given index?

Totality: total
Visibility: public export
elemNotInRest : (DPairtype (AtIndexxxs) ->Void) ->DPairtype (AtIndex (FSx) (y::xs)) ->Void
Totality: total
Visibility: public export
index : DecEqtype=> (idx : Finn) -> (xs : Vectntype) ->Dec (DPairtype (AtIndexidxxs))
  What is the element at the given index?

Totality: total
Visibility: public export