Idris2Doc : Data.Vect

# Data.Vect

## Reexports

`import public Data.Finimport public Data.Zippable`

## Definitions

`data Vect : Nat -> Type -> Type`
Totality: total
Visibility: public export
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`.`

Hints:
`Applicative (Vect k)`
`Biinjective (::)`
`DecEq a => DecEq (Vect n a)`
`Eq a => Eq (Vect n a)`
`Foldable (Vect n)`
`Functor (Vect n)`
`Injective ((x ::))`
`Injective (\x => x :: xs)`
`Monad (Vect k)`
`Monoid a => Monoid (Vect k a)`
`Ord elem => Ord (Vect len elem)`
`Semigroup a => Semigroup (Vect k a)`
`Show elem => Show (Vect len elem)`
`Traversable (Vect k)`
`Zippable (Vect k)`
`length : Vect len elem -> Nat`
Totality: total
Visibility: public export
`lengthCorrect : (xs : Vect len elem) -> length xs = len`
`  Show that the length function on vectors in fact calculates the length`

Totality: total
Visibility: export
`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
Visibility: public export
`head : Vect (S len) elem -> elem`
`  Only the first element of the vector    ```idris example  head [1,2,3,4]  ````

Totality: total
Visibility: public export
`last : Vect (S len) elem -> elem`
`  The last element of the vector    ```idris example  last [1,2,3,4]  ````

Totality: total
Visibility: public export
`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
Visibility: public export
`take : (n : Nat) -> Vect (n + m) type -> Vect n type`
`  Extract the first `n` elements of a Vect.`

Totality: total
Visibility: public export
`take : (n : Nat) -> Stream a -> Vect n a`
`  Take precisely n elements from the stream.  @ n how many elements to take  @ xs the stream`

Totality: total
Visibility: public export
`drop : (n : Nat) -> Vect (n + m) elem -> Vect m elem`
`  Drop the first `n` elements of a Vect.`

Totality: total
Visibility: public export
`drop' : (n : Nat) -> Vect l elem -> Vect (minus l n) elem`
`  Drop up to the first `n` elements of a Vect.`

Totality: total
Visibility: public export
`index : Fin len -> Vect len elem -> elem`
`  Extract a particular element from a vector    ```idris example  index 1 [1,2,3,4]  ````

Totality: total
Visibility: public export
`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
Visibility: public export
`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
Visibility: public export
`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
Visibility: public export
`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
Visibility: public export
`(++) : Vect m elem -> Vect n elem -> Vect (m + n) elem`
`  Append two vectors    ```idris example  [1,2,3,4] ++ [5,6]  ````

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 7
`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
Visibility: public export
`unsnoc : Vect (S n) a -> (Vect n a, a)`
`  Pop the last element from a vector. This is the opposite of `snoc`, in that  `(uncurry snoc) unsnoc xs` is `xs`. It is equivalent to `(init xs, last xs)`,  but traverses the vector once.    @ xs The vector to pop the element from.`

Totality: total
Visibility: public export
`replicate : (len : Nat) -> elem -> Vect len elem`
`  Repeat 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
Visibility: public export
`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
Visibility: export
`merge : Ord elem => Vect n elem -> Vect m elem -> Vect (n + m) elem`
Totality: total
Visibility: export
`replaceAtSameIndex : (xs : Vect n a) -> (i : Fin n) -> (0 y : a) -> index i (replaceAt i y xs) = y`
Totality: total
Visibility: export
`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
Visibility: export
`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
Visibility: public export
`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
Visibility: export
`toVect : (n : Nat) -> List a -> Maybe (Vect n a)`
Totality: total
Visibility: public export
`fromList' : Vect len elem -> (l : List elem) -> Vect (length l + len) elem`
Totality: total
Visibility: public export
`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
Visibility: public export
`mapMaybe : (a -> Maybe b) -> Vect len 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    ```idris example  mapMaybe ((find (=='a')) . unpack) (fromList ["abc","ade","bgh","xyz"])  ````

Totality: total
Visibility: export
`foldrImpl : (t -> acc -> acc) -> acc -> (acc -> acc) -> Vect n t -> acc`
Totality: total
Visibility: public export
`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
Visibility: public export
`foldr1 : (t -> t -> t) -> Vect (S n) t -> t`
`  Foldr without seeding the accumulator    ```idris example  foldr1 (-) (fromList [1,2,3])  ````

Totality: total
Visibility: public export
`foldl1 : (t -> t -> t) -> Vect (S n) t -> t`
`  Foldl without seeding the accumulator    ```idris example  foldl1 (-) (fromList [1,2,3])  ````

Totality: total
Visibility: public export
`scanr : (elem -> res -> res) -> res -> Vect len elem -> Vect (S len) res`
`  The scanr function is similar to foldr, but returns all the intermediate  accumulator states in the form of a vector. Note the intermediate accumulator  states appear in the result in reverse order - the first state appears last  in the result.    ```idris example  scanr (-) 0 (fromList [1,2,3])  ````

Totality: total
Visibility: public export
`scanr1 : (elem -> elem -> elem) -> Vect len elem -> Vect len elem`
`  The scanr1 function is a variant of scanr that doesn't require an explicit  starting value.  It assumes the last element of the vector to be the starting value and then  starts the fold with the element preceding it.    ```idris example  scanr1 (-) (fromList [1,2,3])  ````

Totality: total
Visibility: public export
`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
Visibility: public export
`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
Visibility: public export
`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
Visibility: public export
`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
Visibility: public export
`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
Visibility: public export
`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
Visibility: public export
`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
Visibility: public export
`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
Visibility: public export
`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
Visibility: public export
`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
Visibility: public export
`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
Visibility: public export
`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
Visibility: public export
`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
Visibility: public export
`filter : (elem -> Bool) -> Vect len elem -> (p : Nat ** Vect p elem)`
`  Find all elements of a vector that satisfy some test    ```idris example  filter (< 3) (fromList [1,2,3,4])  ````

Totality: total
Visibility: public export
`nubBy : (elem -> elem -> Bool) -> Vect len elem -> (p : Nat ** 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
Visibility: public export
`nub : Eq elem => Vect len elem -> (p : Nat ** 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
Visibility: public export
`deleteBy : (elem -> elem -> Bool) -> elem -> Vect len elem -> (p : Nat ** 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
Visibility: public export
`delete : Eq elem => elem -> Vect len elem -> (p : Nat ** 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
Visibility: public export
`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
Visibility: public export
`partition : (elem -> Bool) -> Vect len elem -> ((p : Nat ** Vect p elem), (q : Nat ** 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
Visibility: public export
`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
Visibility: public export
`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
Visibility: public export
`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
Visibility: public export
`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
Visibility: public export
`maybeToVect : Maybe elem -> (p : Nat ** Vect p elem)`
`  Convert Maybe type into Vect    ```idris example  maybeToVect (Just 2)  ````

Totality: total
Visibility: public export
`vectToMaybe : Vect len elem -> Maybe elem`
`  Convert first element of Vect (if exists) into Maybe.    ```idris example  vectToMaybe   ````

Totality: total
Visibility: public export
`catMaybes : Vect n (Maybe elem) -> (p : Nat ** 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
Visibility: public export
`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
Visibility: public export
`tabulate : (Fin len -> a) -> Vect len a`
Totality: total
Visibility: public export
`range : Vect len (Fin len)`
Totality: total
Visibility: public export
`tabulate : (Subset Nat (\{arg:0} => LT {arg:0} len) -> a) -> Vect len a`
Totality: total
Visibility: public export
`range : Vect len (Subset Nat (\{arg:0} => LT {arg:0} len))`
Totality: total
Visibility: public export
`zipWithIndexLinear : (0 f : (a -> a -> {a:8859})) -> (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
Visibility: export
`zipWith3IndexLinear : (0 f : (a -> a -> a -> {a:8962})) -> (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
Visibility: export
`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
Visibility: public export
`exactLength : (len : Nat) -> Vect m a -> Maybe (Vect len a)`
Totality: total
Visibility: export
`overLength : (len : Nat) -> 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`

Totality: total
Visibility: export