- (++) : Vect m elem -> Vect n elem -> Vect (m + n) elem
Append two vectors
```idris example
[1,2,3,4] ++ [5,6]
```
Totality: total
Fixity Declaration: infixr operator, level 7- data Vect : Nat -> Type -> Type
- Totality: total
Constructors:
- Nil : Vect 0 elem
Empty vector
- (::) : elem -> Vect len elem -> Vect (S len) elem
A non-empty vector of length `S len`, consisting of a head element and
the rest of the list, of length `len`.
- catMaybes : Vect n (Maybe elem) -> DPair Nat (\p => Vect p elem)
Filter out Nothings from Vect and unwrap the Justs
```idris example
catMaybes [Just 1, Just 2, Nothing, Nothing, Just 5]
```
Totality: total- concat : Vect m (Vect n elem) -> Vect (m * n) elem
Flatten a vector of equal-length vectors
```idris example
concat [[1,2,3], [4,5,6]]
```
Totality: total- delete : Eq elem => elem -> Vect len elem -> DPair Nat (\p => Vect p elem)
Delete first element from list equal to the given one
```idris example
delete 2 (fromList [1,2,2,3,4,4])
```
Totality: total- deleteAt : Fin (S len) -> Vect (S len) elem -> Vect len elem
Construct a new vector consisting of all but the indicated element
```idris example
deleteAt 1 [1,2,3,4]
```
Totality: total- deleteBy : (elem -> elem -> Bool) -> elem -> Vect len elem -> DPair Nat (\p => Vect p elem)
Delete first element from list according to some test
```idris example
deleteBy (<) 3 (fromList [1,2,2,3,4,4])
```
Totality: total- diag : Vect len (Vect len elem) -> Vect len elem
Get diagonal elements
```idris example
diag [[1,2,3], [4,5,6], [7,8,9]]
```
Totality: total- drop : (n : Nat) -> Vect (n + m) elem -> Vect m elem
Drop the first `n` elements of a Vect.
Totality: total- drop' : (n : Nat) -> Vect l elem -> Vect (minus l n) elem
Drop up to the first `n` elements of a Vect.
Totality: total- elem : Eq elem => elem -> Vect len elem -> Bool
Use the default Boolean equality on elements to search for an item
@ x what to search for
@ xs where to search
```idris example
elem 3 [1,2,3,4]
```
Totality: total- elemBy : (elem -> elem -> Bool) -> elem -> Vect len elem -> 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
```idris example
elemBy (==) 2 [1,2,3,4]
```
Totality: total- elemIndex : Eq elem => elem -> Vect m elem -> Maybe (Fin m)
Find the index of the first element of the vector equal to the given one.
```idris example
elemIndex 3 [1,2,3,4]
```
Totality: total- elemIndexBy : (elem -> elem -> Bool) -> elem -> Vect m elem -> Maybe (Fin m)
Find the index of the first element of the vector that satisfies some test
```idris example
elemIndexBy (==) 3 [1,2,3,4]
```
Totality: total- elemIndices : Eq elem => elem -> Vect m elem -> List (Fin m)
Find the indices of all elements uquals to the given one
```idris example
elemIndices 3 [1,2,3,4,3]
```
Totality: total- elemIndicesBy : (elem -> elem -> Bool) -> elem -> Vect m elem -> List (Fin m)
Find the indices of all elements that satisfy some test
```idris example
elemIndicesBy (<=) 3 [1,2,3,4]
```
Totality: total- exactLength : (len : Nat) -> Vect m a -> Maybe (Vect len a)
- Totality: total
- filter : (elem -> Bool) -> Vect len elem -> DPair Nat (\p => Vect p elem)
Find all elements of a vector that satisfy some test
```idris example
filter (< 3) (fromList [1,2,3,4])
```
Totality: total- find : (elem -> Bool) -> Vect len elem -> Maybe elem
Find the first element of the vector that satisfies some test
@ p the test to satisfy
```idris example
find (== 3) [1,2,3,4]
```
Totality: total- findIndex : (elem -> Bool) -> Vect len elem -> Maybe (Fin len)
Find the index of the first element of the vector that satisfies some test
```idris example
findIndex (== 3) [1,2,3,4]
```
Totality: total- findIndices : (elem -> Bool) -> Vect m elem -> List (Fin m)
Find the indices of all elements that satisfy some test
```idris example
findIndices (< 3) [1,2,3,4]
```
Totality: total- foldl1 : (t -> t -> t) -> Vect (S n) t -> t
Foldl without seeding the accumulator
```idris example
foldl1 (-) (fromList [1,2,3])
```
Totality: total- foldr1 : (t -> t -> t) -> Vect (S n) t -> t
Foldr without seeding the accumulator
```idris example
foldr1 (-) (fromList [1,2,3])
```
Totality: total- foldrImpl : (t -> acc -> acc) -> acc -> (acc -> acc) -> Vect n t -> acc
- Totality: total
- fromList : (xs : List elem) -> Vect (length xs) elem
Convert a list to a vector.
The length of the list should be statically known.
```idris example
fromList [1,2,3,4]
```
Totality: total- fromList' : Vect len elem -> (l : List elem) -> Vect (length l + len) elem
- Totality: total
- hasAny : Eq elem => Vect m elem -> Vect len elem -> Bool
Check if any element of xs is found in elems using the default Boolean equality test
```idris example
hasAny [2,5] [1,2,3,4]
```
Totality: total- hasAnyBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> 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
```idris example
hasAnyBy (==) [2,5] [1,2,3,4]
```
Totality: total- head : Vect (S len) elem -> elem
Only the first element of the vector
```idris example
head [1,2,3,4]
```
Totality: total- index : Fin len -> Vect len elem -> elem
Extract a particular element from a vector
```idris example
index 1 [1,2,3,4]
```
Totality: total- init : Vect (S len) elem -> Vect len elem
All but the last element of the vector
```idris example
init [1,2,3,4]
```
Totality: total- insertAt : Fin (S len) -> elem -> Vect len elem -> Vect (S len) elem
Insert an element at a particular index
```idris example
insertAt 1 8 [1,2,3,4]
```
Totality: total- intersperse : elem -> Vect len elem -> Vect (len + pred len) elem
Alternate an element between the other elements of a vector
@ sep the element to intersperse
@ xs the vector to separate with `sep`
```idris example
intersperse 0 [1,2,3,4]
```
Totality: total- isPrefixOf : Eq elem => Vect m elem -> Vect len elem -> Bool
Verify vector prefix
```idris example
isPrefixOf (fromList [1,2]) (fromList [1,2,3,4])
```
Totality: total- isPrefixOfBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> Bool
Verify vector prefix
```idris example
isPrefixOfBy (==) (fromList [1,2]) (fromList [1,2,3,4])
```
Totality: total- isSuffixOf : Eq elem => Vect m elem -> Vect len elem -> Bool
Verify vector suffix
```idris example
isSuffixOf (fromList [3,4]) (fromList [1,2,3,4])
```
Totality: total- isSuffixOfBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> Bool
Verify vector suffix
```idris example
isSuffixOfBy (==) (fromList [3,4]) (fromList [1,2,3,4])
```
Totality: total- last : Vect (S len) elem -> elem
The last element of the vector
```idris example
last [1,2,3,4]
```
Totality: total- length : Vect len elem -> Nat
- Totality: total
- lengthCorrect : (xs : Vect len elem) -> length xs = len
Show that the length function on vectors in fact calculates the length
Totality: total- lookup : Eq key => key -> Vect n (key, val) -> Maybe val
Find the assocation of some key using the default Boolean equality test
```idris example
lookup 3 [(1, 'a'), (2, 'b'), (3, 'c')]
```
Totality: total- lookupBy : (key -> key -> Bool) -> key -> Vect n (key, val) -> Maybe val
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
```idris example
lookupBy (==) 2 [(1, 'a'), (2, 'b'), (3, 'c')]
```
Totality: total- mapMaybe : (a -> Maybe b) -> Vect len a -> DPair Nat (\m => 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
```idris example
mapMaybe ((find (=='a')) . unpack) (fromList ["abc","ade","bgh","xyz"])
```
Totality: total- maybeToVect : Maybe elem -> DPair Nat (\p => Vect p elem)
Convert Maybe type into Vect
```idris example
maybeToVect (Just 2)
```
Totality: total- merge : Ord elem => Vect n elem -> Vect m elem -> Vect (n + m) elem
- Totality: total
- mergeBy : (elem -> elem -> Ordering) -> Vect n elem -> Vect m elem -> Vect (n + m) elem
Merge two ordered vectors
```idris example
mergeBy compare (fromList [1,3,5]) (fromList [2,3,4,5,6])
```
Totality: total- nub : Eq elem => Vect len elem -> DPair Nat (\p => Vect p elem)
Make the elements of some vector unique by the default Boolean equality
```idris example
nub (fromList [1,2,2,3,4,4])
```
Totality: total- nubBy : (elem -> elem -> Bool) -> Vect len elem -> DPair Nat (\p => Vect p elem)
Make the elements of some vector unique by some test
```idris example
nubBy (==) (fromList [1,2,2,3,4,4])
```
Totality: total- overLength : (len : Nat) -> Vect m a -> Maybe (DPair Nat (\p => 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
Totality: total- partition : (elem -> Bool) -> Vect len elem -> (DPair Nat (\p => Vect p elem), DPair Nat (\q => Vect q elem))
A tuple where the first element is a `Vect` of the `n` elements passing given test
and the second element is a `Vect` of the remaining elements of the original.
```idris example
partition (== 2) (fromList [1,2,3,2,4])
```
Totality: total- replaceAt : Fin len -> elem -> Vect len elem -> Vect len elem
Replace an element at a particlar index with another
```idris example
replaceAt 1 8 [1,2,3,4]
```
Totality: total- replaceAtDiffIndexPreserves : (xs : Vect n a) -> (i : Fin n) -> (j : Fin n) -> Not (i = j) -> (0 y : a) -> index i (replaceAt j y xs) = index i xs
- Totality: total
- replaceAtSameIndex : (xs : Vect n a) -> (i : Fin n) -> (0 y : a) -> index i (replaceAt i y xs) = y
- Totality: total
- replicate : (len : Nat) -> elem -> Vect len elem
Repeate some value some number of times.
@ len the number of times to repeat it
@ x the value to repeat
```idris example
replicate 4 1
```
Totality: total- reverse : Vect len elem -> Vect len elem
Reverse the order of the elements of a vector
```idris example
reverse [1,2,3,4]
```
Totality: total- scanl : (res -> elem -> res) -> res -> Vect len elem -> Vect (S len) res
The scanl function is similar to foldl, but returns all the intermediate
accumulator states in the form of a vector.
```idris example
scanl (-) 0 (fromList [1,2,3])
```
Totality: total- scanl1 : (elem -> elem -> elem) -> Vect len elem -> Vect len elem
The scanl1 function is a variant of scanl that doesn't require an explicit
starting value.
It assumes the first element of the vector to be the starting value and then
starts the fold with the element following it.
```idris example
scanl1 (-) (fromList [1,2,3])
```
Totality: total- snoc : Vect n a -> a -> Vect (S n) a
Add an element at the end of the vector.
The main use case for it is to get the expected type signature
`Vect n a -> a -> Vect (S n) a` instead of
`Vect n a -> a -> Vect (n + 1) a` which you get by using `++ [x]`
Snoc gets its name by reversing `cons`, indicating we are
tacking on the element at the end rather than the begining.
`append` would also be a suitable name.
@ xs The vector to be appended
@ v The value to append
Totality: total- splitAt : (n : Nat) -> Vect (n + m) elem -> (Vect n elem, Vect m elem)
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.
It is equivalent to `(take n xs, drop n xs)` (`splitAtTakeDrop`),
but is more efficient.
@ n the index to split at
@ xs the `Vect` to split in two
```idris example
splitAt 2 (fromList [1,2,3,4])
```
Totality: total- tail : Vect (S len) elem -> Vect len elem
All but the first element of the vector
```idris example
tail [1,2,3,4]
```
Totality: total- take : (n : Nat) -> Vect (n + m) type -> Vect n type
Extract the first `n` elements of a Vect.
Totality: total- toVect : (n : Nat) -> List a -> Maybe (Vect n a)
- Totality: total
- transpose : Vect m (Vect n elem) -> Vect n (Vect m elem)
Transpose a `Vect` of `Vect`s, turning rows into columns and vice versa.
This is like zipping all the inner `Vect`s together and is equivalent to `traverse id` (`transposeTraverse`).
As the types ensure rectangularity, this is an involution, unlike `Prelude.List.transpose`.
```idris example
transpose [[1,2], [3,4], [5,6], [7,8]]
```
Totality: total- updateAt : Fin len -> (elem -> elem) -> Vect len elem -> Vect len elem
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
```idris example
updateAt 1 (+10) [1,2,3,4]
```
Totality: total- vectInjective : x :: xs = y :: ys -> (x = y, xs = ys)
If two vectors are equal, their heads and tails are equal
Totality: total- vectToMaybe : Vect len elem -> Maybe elem
Convert first element of Vect (if exists) into Maybe.
```idris example
vectToMaybe [2]
```
Totality: total- zipWith3IndexLinear : (0 f : (a -> a -> a -> a)) -> (xs : Vect n a) -> (ys : Vect n a) -> (zs : Vect n a) -> (i : Fin n) -> index i (zipWith3 f xs ys zs) = f (index i xs) (index i ys) (index i zs)
- Totality: total
- zipWithIndexLinear : (0 f : (a -> a -> a)) -> (xs : Vect n a) -> (ys : Vect n a) -> (i : Fin n) -> index i (zipWith f xs ys) = f (index i xs) (index i ys)
- Totality: total