Documentation

Add an element to the tail of the vector

Extract the first element of a vector

Extract the elements after the head of a vector

Extract the last element of a vector

Extract all the elements of a vector except the last element

Add an element to the head of the vector, and extract all elements of the resulting vector except the last element

Add an element to the tail of the vector, and extract all elements of the resulting vector except the first element

Append two vectors

Concatenate a vector of vectors

Split a vector into two vectors at the given point

Split a vector into two vectors where the length of the two is determined by the context

Split a vector of (n * m) elements into a vector of vectors with length m, where m is given

Split a vector of (n * m) elements into a vector of vectors with length m, where m is determined by the context

Merge two vectors, alternating their elements, i.e.,

vmerge <xn, ..., x2, x1>  <yn, ..., y2, y1> == <xn, yn, ..., x2, y2, x1, y1>

Returns the elements in a list in reverse order

vmap f xs is the list obtained by applying f to each element of xs, i.e.,

vmap f <xn, ..., x2, x1> == <f xn, ..., f x2, f x1>

vzipWith generalises vzip by zipping with the function given as the first argument, instead of a tupling function. For example, vzipWith (+) is applied to two vectors to produce the vector of corresponding sums.

vfoldr, applied to a binary operator, a starting value (typically the right-identity of the operator), and a vector, reduces the vector using the binary operator, from right to left:

foldr f z <xn, ..., x2, x1> == xn `f` (... (x2 `f` (x1 `f` z))...)

vfoldl, applied to a binary operator, a starting value (typically the left-identity of the operator), and a vector, reduces the vector using the binary operator, from left to right:

vfoldl f z <xn, ..., x2, x1> == (...((z `f` xn)... `f` x2) `f` x1

vfoldr1 is a variant of vfoldr that has no starting value argument, and thus must be applied to non-empty vectors.

vfoldl1 is a variant of vfoldl that has no starting value argument, and thus must be applied to non-empty vectors.

vzip takes two lists and returns a list of corresponding pairs.

vunzip transforms a list of pairs into a list of first components and a list of second components.

Vector index (subscript) operator, descending from maxIndex, where the last element has subscript 0.

<1,2,3,4,5> ! 4 == 1
<1,2,3,4,5> ! maxIndex == 1
<1,2,3,4,5> ! 1 == 4

Replace an element of a vector at the given index (subscript), NB: vector elements have a descending subscript starting from maxIndex and ending at 0

vreplace <1,2,3,4,5> 3 7 == <1,7,3,4,5>

Index (subscript) of the head of the vector

vtake n, applied to a vector xs, returns the n-length prefix of xs

vtake (snat :: SNat 3) <1,2,3,4,5> == <1,2,3>
vtake d3 <1,2,3,4,5> == <1,2,3>
vtake (snat :: SNat 0) <1,2> == <>
vtake (snat :: SNat 4) <1,2> == TYPE ERROR

vtakeI xs, returns the prefix of xs as demanded by the context

vdrop n xs returns the suffix of xs after the first n elements

vdrop (snat :: SNat 3) <1,2,3,4,5> == <4,5>
vdrop d3 <1,2,3,4,5> == <4,5>
vdrop (snat :: SNat 0) <1,2> == <1,2>
vdrop (snat :: SNat 4) <1,2> == TYPE ERROR

vdropI xs, returns the suffix of xs as demanded by the context

vexact n xs returns n'th element of xs, NB: vector elements have a descending subscript starting from maxIndex and ending at 0

vexact (snat :: SNat 1) <1,2,3,4,5> == 4

vselect f s n xs selects n elements with stepsize s and offset f from xs

vselect (snat :: SNat 1) (snat :: SNat 2) (snat :: SNat 3) 1,2,3,4,5,6,7,8 == 2,4,6

vselectI f s xs selects as many elements as demanded by the context with stepsize s and offset f from xs

vcopy n a returns a vector that has n copies of a

vcopy a creates a vector with as many copies of a as demanded by the context

viterate n f x returns a vector starting with x followed by n repeated applications of f to x

viterate (snat :: SNat 4) f x = <x, f x, f (f x), f (f (f x))>

viterate f x returns a vector starting with x followed by n repeated applications of f to x, where n is determined by the context

vgenerate n f x returns a vector with n repeated applications of f to x

vgenerate (snat :: SNat 4) f x = <f x, f (f x), f (f (f x)), f (f (f (f x)))>

vgenerate f x returns a vector with n repeated applications of f to x, where n is determined by the context

Convert a vector to a list

Create a vector literal from a list literal

$(v [1::Signed 8,2,3,4,5]) == <1,2,3,4,5> :: Vec 5 (Signed 8)