Data.Vect

zipWith3 : (a -> b -> c -> d) -> Vect n a -> Vect n b -> Vect n c -> Vect n d

Combine three equal-length vectors into a vector with some function

zipWith : (f : a -> b -> c) -> (xs : Vect n a) -> (ys : Vect n b) -> Vect n c

Combine two equal-length vectors pairwise with some function.

f

the function to combine elements with

xs

the first vector of elements

ys

the second vector of elements

zip3 : Vect n a -> Vect n b -> Vect n c -> Vect n (a, b, c)

Combine three equal-length vectors elementwise into a vector of tuples

zip : Vect n a -> Vect n b -> Vect n (a, b)

Combine two equal-length vectors pairwise

vectToMaybe : Vect n a -> Maybe a

vectNilRightNeutral : (xs : Vect n a) -> xs ++ [] = xs

vectInjective2 : (x :: xs = y :: ys) -> xs = ys

vectInjective1 : (x :: xs = y :: ys) -> x = y

vectConsCong : (x : a) -> (xs : Vect n a) -> (ys : Vect m a) -> (xs = ys) -> x :: xs = x :: ys

vectAppendAssociative : (x : Vect xLen a) -> (y : Vect yLen a) -> (z : Vect zLen a) -> x ++ y ++ z = (x ++ y) ++ z

updateAt : (i : Fin n) -> (f : t -> t) -> (xs : Vect n t) -> Vect n t

Replace the element at a particular index with the result of applying a function to it

i

the index to replace at

f

the update function

xs

the vector to replace in

unzip3 : Vect n (a, b, c) -> (Vect n a, Vect n b, Vect n c)

Convert a vector of three-tuples to a triplet of vectors

unzip : Vect n (a, b) -> (Vect n a, Vect n b)

Convert a vector of pairs to a pair of vectors

transpose : Vect m (Vect n a) -> Vect n (Vect m a)

Transpose a Vect of Vects, turning rows into columns and vice versa.

As the types ensure rectangularity, this is an involution, unlike Prelude.List.transpose.

takeWhile : (p : a -> Bool) -> Vect n a -> (q : Nat ** Vect q a)

Take the longest prefix of a Vect such that all elements satisfy some
Boolean predicate.

p

the predicate

take : (n : Nat) -> Vect (n + m) a -> Vect n a

Get the first n elements of a Vect

n

the number of elements to take

tail : Vect (S n) a -> Vect n a

All but the first element of the vector

splitAt : (n : Nat) -> (xs : Vect (n + m) a) -> (Vect n a, Vect m a)

A tuple where the first element is a Vect of the n first elements and
the second element is a Vect of the remaining elements of the original Vect
It is equivalent to (take n xs, drop n xs)

n

the index to split at

xs

the Vect to split in two

scanl : (b -> a -> b) -> b -> Vect n a -> Vect (S n) b

reverse : Vect n a -> Vect n a

Reverse the order of the elements of a vector

replicate : (n : Nat) -> (x : a) -> Vect n a

Repeate some value n times

n

the number of times to repeat it

x

the value to repeat

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

replaceAt : Fin n -> t -> Vect n t -> Vect n t

Replace an element at a particlar index with another

range : Vect n (Fin n)

partition : (a -> Bool) -> Vect n a -> ((p : Nat ** Vect p a), (q : Nat ** Vect q a))

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

nubBy : (a -> a -> Bool) -> Vect n a -> (p : Nat ** Vect p a)

Make the elements of some vector unique by some test

nub : Eq a => Vect n a -> (p : Nat ** Vect p a)

Make the elements of some vector unique by the default Boolean equality

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

mergeBy : (a -> a -> Ordering) -> Vect n a -> Vect m a -> Vect (n + m) a

Merge two ordered vectors

merge : Ord a => Vect n a -> Vect m a -> Vect (n + m) a

maybeToVect : Maybe a -> (p : Nat ** Vect p a)

mapMaybe : (f : a -> Maybe b) -> (xs : Vect n a) -> (m : Nat ** Vect m b)

Map a partial function across a vector, returning those elements for which
the function had a value.

The first projection of the resulting pair (ie the length) will always be
at most the length of the input vector. This is not, however, guaranteed
by the type.

f

the partial function (expressed by returning Maybe)

xs

the vector to check for results

mapElem : Elem x xs -> Elem (f x) (map f xs)

lookupBy : (p : a -> a -> Bool) -> (e : a) -> (xs : Vect n (a, b)) -> Maybe b

Find the association of some key with a user-provided comparison

p

the comparison operator for keys (True if they match)

e

the key to look for

lookup : Eq a => a -> Vect n (a, b) -> Maybe b

Find the assocation of some key using the default Boolean equality test

length : (xs : Vect n a) -> Nat

Calculate the length of a Vect.

Note: this is only useful if you don't already statically know the length
and you want to avoid matching the implicit argument for erasure reasons.

n

the length (provably equal to the return value)

xs

the vector

last : Vect (S n) a -> a

The last element of the vector

isSuffixOfBy : (a -> a -> Bool) -> Vect m a -> Vect n a -> Bool

isSuffixOf : Eq a => Vect m a -> Vect n a -> Bool

isPrefixOfBy : (a -> a -> Bool) -> Vect m a -> Vect n a -> Bool

isPrefixOf : Eq a => Vect m a -> Vect n a -> Bool

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

A decision procedure for Elem

intersperse : (sep : a) -> (xs : Vect n a) -> Vect (n + pred n) a

Alternate an element between the other elements of a vector

sep

the element to intersperse

xs

the vector to separate with sep

insertAt : Fin (S n) -> a -> Vect n a -> Vect (S n) a

Insert an element at a particular index

init : Vect (S n) a -> Vect n a

All but the last element of the vector

index : Fin n -> Vect n a -> a

Extract a particular element from a vector

head : Vect (S n) a -> a

Only the first element of the vector

hasAnyBy : (p : a -> a -> Bool) -> (elems : Vect m a) -> (xs : Vect n a) -> Bool

Check if any element of xs is found in elems by a user-provided comparison

p

the comparison operator

elems

the vector to search

xs

what to search for

hasAny : Eq a => Vect m a -> Vect n a -> Bool

Check if any element of xs is found in elems using the default Boolean equality test

fromList' : Vect n a -> (l : List a) -> Vect (length l + n) a

fromList : (l : List a) -> Vect (length l) a

Convert a list to a vector.

The length of the list should be statically known.

foldrImpl : (t -> acc -> acc) -> acc -> (acc -> acc) -> Vect n t -> acc

foldr1 : (t -> t -> t) -> Vect (S n) t -> t

Foldr without seeding the accumulator

foldl1 : (t -> t -> t) -> Vect (S n) t -> t

Foldl without seeding the accumulator

findIndices : (a -> Bool) -> Vect m a -> List (Fin m)

Find the indices of all elements that satisfy some test

findIndex : (a -> Bool) -> Vect n a -> Maybe (Fin n)

Find the index of the first element of the vector that satisfies some test

find : (p : a -> Bool) -> (xs : Vect n a) -> Maybe a

Find the first element of the vector that satisfies some test

p

the test to satisfy

filter : (a -> Bool) -> Vect n a -> (p : Nat ** Vect p a)

Find all elements of a vector that satisfy some test

exactLength : (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

elemIndicesBy : (a -> a -> Bool) -> a -> Vect m a -> List (Fin m)

elemIndices : Eq a => a -> Vect m a -> List (Fin m)

elemIndexBy : (a -> a -> Bool) -> a -> Vect m a -> Maybe (Fin m)

elemIndex : Eq a => a -> Vect m a -> Maybe (Fin m)

elemBy : (p : a -> a -> Bool) -> (e : a) -> (xs : Vect n a) -> Bool

Search for an item using a user-provided test

p

the equality test

e

the item to search for

xs

the vector to search in

elem : Eq a => (x : a) -> (xs : Vect n a) -> Bool

Use the default Boolean equality on elements to search for an item

x

what to search for

xs

where to search

dropWhile : (p : a -> Bool) -> Vect n a -> (q : Nat ** Vect q a)

Remove the longest prefix of a Vect such that all removed elements satisfy some
Boolean predicate.

p

the predicate

drop : (n : Nat) -> Vect (n + m) a -> Vect m a

Remove the first n elements of a Vect

n

the number of elements to remove

diag : Vect n (Vect n a) -> Vect n a

deleteBy : (a -> a -> Bool) -> a -> Vect n a -> (p : Nat ** Vect p a)

deleteAt : Fin (S n) -> Vect (S n) a -> Vect n a

Construct a new vector consisting of all but the indicated element

delete : Eq a => a -> Vect n a -> (p : Nat ** Vect p a)

concat : Vect m (Vect n a) -> Vect (m * n) a

Flatten a vector of equal-length vectors

catMaybes : Vect n (Maybe a) -> (p : Nat ** Vect p a)

data Vect : Nat -> Type -> Type

Vectors: Generic lists with explicit length in the type

Nil : Vect 0 a

Empty vector

(::) : (x : a) -> (xs : Vect k a) -> Vect (S k) a

A non-empty vector of length S k, consisting of a head element and
the rest of the list, of length k.

Fixity

Left associative, precedence 7

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

A proof that some element is found in a vector

Here : Elem x (x :: xs)

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

(++) : Vect m a -> Vect n a -> Vect (m + n) a

Append two vectors

Fixity

Left associative, precedence 7