Idris2Doc : Data.Vect.Elem

Data.Vect.Elem

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

  Totality: total
  Constructors:
  
Here : Elem x (x :: xs)
  
There : Elem x xs -> Elem x (y :: xs)
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
elemToFin : Elem x xs -> Fin n
  Erase the indices, returning the bounded numeric position of the element

  Totality: total
indexElem : (1 _ : Fin n) -> (xs : Vect n a) -> DPair a (\x => Elem x xs)
  Find the element with a proof at a given bounded position

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

  Totality: total
mapElem : (1 _ : Elem x xs) -> Elem (f x) (map f xs)
  Totality: total
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
replaceByElem : (xs : Vect k t) -> Elem x xs -> t -> Vect k t
  Totality: total
replaceElem : (xs : Vect k t) -> Elem x xs -> (y : t) -> DPair (Vect k t) (\ys => Elem y ys)
  Totality: total