IdrisDoc: Data.VectType.Vect

# Data.VectType.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 : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c

Combine two equal-length vectors pairwise with some function

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
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

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))
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

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 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

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
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 -> (p : Nat ** Vect p Nat)

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

elemIndicesBy : (a -> a -> Bool) -> a -> Vect m a -> (p : Nat ** Vect p Nat)
elemIndices : Eq a => a -> Vect m a -> (p : Nat ** Vect p Nat)
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
(++) : Vect m a -> Vect n a -> Vect (m + n) a

Append two vectors

Fixity
Left associative, precedence 7