IdrisDoc: Data.Vect

# Data.Vect

replaceElem : (xs : Vect k t) -> Elem x xs -> (y : t) -> (ys : Vect k t ** Elem y ys)
replaceByElem : (xs : Vect k t) -> Elem x xs -> t -> Vect k t
overLength : (len : Nat) -> (xs : Vect m a) -> Maybe (p : Nat ** Vect (plus p len) a)

If the given Vect is at least the required length, return a Vect with
at least that length in its type, otherwise return Nothing

len

the required length

xs

the vector with the desired length

noEmptyElem : Elem x [] -> Void

Nothing can be in an empty Vect

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

mapElem : Elem x xs -> Elem (f x) (map f xs)
isLength : (len : Nat) -> (xs : Vect m a) -> Maybe (Vect len a)

If the given Vect is the required length, return a Vect with that
length in its type, otherwise return Nothing

len

the required length

xs

the vector with the desired length

isElem : DecEq a => (x : a) -> (xs : Vect n a) -> Dec (Elem x xs)

A decision procedure for Elem

findElem : (n : Nat) -> List (TTName, Binder TT) -> TT -> Tactic

A tactic for discovering where, if anywhere, an element is in a vector

n

how many elements to search before giving up

data Elem : a -> Vect k a -> Type

A proof that some element is found in a vector

Here : Elem x (x :: xs)
There : Elem x xs -> Elem x (y :: xs)