Idris2Doc : Data.Vect.Elem

Data.Vect.Elem

Definitions

`data Elem : a -> Vect k a -> Type`
`  A proof that some element is found in a vector`

Totality: total
Visibility: public export
Constructors:
`Here : Elem x (x :: xs)`
`There : Elem x xs -> Elem x (y :: xs)`

Hints:
`DecEq (Elem x xs)`
`Injective There`
`Uninhabited (Here = There e)`
`Uninhabited (There e = Here)`
`Uninhabited (Elem x [])`
`Uninhabited (x = z) => Uninhabited (Elem z xs) => Uninhabited (Elem z (x :: xs))`
`neitherHereNorThere : Not (x = y) -> Not (Elem x xs) -> Not (Elem x (y :: xs))`
`  An item not in the head and not in the tail is not in the Vect at all`

Totality: total
Visibility: export
`isElem : DecEq a => (x : a) -> (xs : Vect n a) -> Dec (Elem x xs)`
`  A decision procedure for Elem`

Totality: total
Visibility: public export
`get : (xs : Vect n a) -> Elem x xs -> a`
`  Get the element at the given position.`

Totality: total
Visibility: public export
`lookup : (xs : Vect n a) -> Elem x xs -> Singleton x`
`  Get the element at the given position, with proof that it is the desired element.`

Totality: total
Visibility: public export
`replaceElem : (xs : Vect k t) -> Elem x xs -> (y : t) -> (ys : Vect k t ** Elem y ys)`
Totality: total
Visibility: public export
`replaceByElem : (xs : Vect k t) -> Elem x xs -> t -> Vect k t`
Totality: total
Visibility: public export
`mapElem : (1 _ : Elem x xs) -> Elem (f x) (map f xs)`
Totality: total
Visibility: public export
`dropElem : (xs : Vect (S k) t) -> Elem x xs -> Vect k t`
`  Remove the element at the given position.    @xs The vector to be removed from  @p A proof that the element to be removed is in the vector`

Totality: total
Visibility: public export
`elemToFin : Elem x xs -> Fin n`
`  Erase the indices, returning the bounded numeric position of the element`

Totality: total
Visibility: public export
`indexElem : (1 _ : Fin n) -> (xs : Vect n a) -> (x : a ** Elem x xs)`
`  Find the element with a proof at a given bounded position`

Totality: total
Visibility: public export