Idris2Doc : Data.Vect.Elem

Data.Vect.Elem

Elem : a -> Vectka -> Type
A proof that some element is found in a vector
Totality: total
Constructors:
Here : Elemx (x::xs)
There : Elemxxs -> Elemx (y::xs)
dropElem : (xs : Vect (Sk) t) -> Elemxxs -> Vectkt
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
elemToFin : Elemxxs -> Finn
Erase the indices, returning the bounded numeric position of the element
indexElem : (1 _ : Finn) -> (xs : Vectna) -> DPaira (\x => Elemxxs)
Find the element with a proof at a given bounded position
isElem : DecEqa => (x : a) -> (xs : Vectna) -> Dec (Elemxxs)
A decision procedure for Elem
mapElem : (1 _ : Elemxxs) -> Elem (fx) (mapfxs)
neitherHereNorThere : Not (x = y) -> Not (Elemxxs) -> Not (Elemx (y::xs))
An item not in the head and not in the tail is not in the Vect at all
replaceByElem : (xs : Vectkt) -> Elemxxs -> t -> Vectkt
replaceElem : (xs : Vectkt) -> Elemxxs -> (y : t) -> DPair (Vectkt) (\ys => Elemyys)