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