Abstract
Utility functions for arrays.
Synopsis
| open import "/prelude/zip" | ||
| val length | [n] 't : | [n]t -> i64 | 
| val null | [n] 't : | [n]t -> bool | 
| val head | [n] 't : | (x: [n]t) -> t | 
| val last | [n] 't : | (x: [n]t) -> t | 
| val tail | [n] 't : | (x: [n]t) -> ?[n₃].[n₃]t | 
| val init | [n] 't : | (x: [n]t) -> ?[n₅].[n₅]t | 
| val take | [n] 't : | (i: i64) -> (x: [n]t) -> [i]t | 
| val drop | [n] 't : | (i: i64) -> (x: [n]t) -> ?[n₂].[n₂]t | 
| val split | [n] 't : | (i: i64) -> (xs: [n]t) -> ([i]t, []t) | 
| val reverse | [n] 't : | (x: [n]t) -> [n]t | 
| val ++ | [n] [m] 't : | (xs: [n]t) -> (ys: [m]t) -> *[]t | 
| val concat | [n] [m] 't : | (xs: [n]t) -> (ys: [m]t) -> *[]t | 
| val concat_to | [n] [m] 't : | (k: i64) -> (xs: [n]t) -> (ys: [m]t) -> *[k]t | 
| val rotate | [n] 't : | (r: i64) -> (xs: [n]t) -> [n]t | 
| val iota | : | (n: i64) -> *[n]i64 | 
| val indices | [n] 't : | [n]t -> *[n]i64 | 
| val replicate | 't : | (n: i64) -> (x: t) -> *[n]t | 
| val copy | 't : | (a: t) -> *t | 
| val flatten | [n] [m] 't : | (xs: [n][m]t) -> []t | 
| val flatten_to | [n] [m] 't : | (l: i64) -> (xs: [n][m]t) -> [l]t | 
| val flatten_3d | [n] [m] [l] 't : | (xs: [n][m][l]t) -> []t | 
| val flatten_4d | [n] [m] [l] [k] 't : | (xs: [n][m][l][k]t) -> []t | 
| val unflatten | [p] 't : | (n: i64) -> (m: i64) -> (xs: [p]t) -> [n][m]t | 
| val unflatten_3d | [p] 't : | (n: i64) -> (m: i64) -> (l: i64) -> (xs: [p]t) -> [n][m][l]t | 
| val unflatten_4d | [p] 't : | (n: i64) -> (m: i64) -> (l: i64) -> (k: i64) -> (xs: [p]t) -> [n][m][l][k]t | 
| val transpose | [n] [m] 't : | (a: [n][m]t) -> [m][n]t | 
| val and | [n] : | (xs: [n]bool) -> bool | 
| val or | [n] : | (xs: [n]bool) -> bool | 
| val foldl | [n] 'a 'b : | (f: a -> b -> a) -> (acc: a) -> (bs: [n]b) -> a | 
| val foldr | [n] 'a 'b : | (f: b -> a -> a) -> (acc: a) -> (bs: [n]b) -> a | 
| val tabulate | 'a : | (n: i64) -> (f: i64 -> a) -> *[n]a | 
| val tabulate_2d | 'a : | (n: i64) -> (m: i64) -> (f: i64 -> i64 -> a) -> *[n][m]a | 
| val tabulate_3d | 'a : | (n: i64) -> (m: i64) -> (o: i64) -> (f: i64 -> i64 -> i64 -> a) -> *[n][m][o]a | 
Description
- ↑val tail [n] 't: (x: [n]t) -> ?[n₃].[n₃]t
- Everything but the first element of the array. - Complexity: O(1). 
- ↑val init [n] 't: (x: [n]t) -> ?[n₅].[n₅]t
- Everything but the last element of the array. - Complexity: O(1). 
- ↑val take [n] 't: (i: i64) -> (x: [n]t) -> [i]t
- Take some number of elements from the head of the array. - Complexity: O(1). 
- ↑val drop [n] 't: (i: i64) -> (x: [n]t) -> ?[n₂].[n₂]t
- Remove some number of elements from the head of the array. - Complexity: O(1). 
- ↑val split [n] 't: (i: i64) -> (xs: [n]t) -> ([i]t, []t)
- Split an array at a given position. - Complexity: O(1). 
- ↑val reverse [n] 't: (x: [n]t) -> [n]t
- Return the elements of the array in reverse order. - Complexity: O(1). 
- ↑val ++ [n] [m] 't: (xs: [n]t) -> (ys: [m]t) -> *[]t
- Concatenate two arrays. Warning: never try to perform a reduction with this operator; it will not work. - Work: O(n). - Span: O(1). 
- ↑val concat_to [n] [m] 't: (k: i64) -> (xs: [n]t) -> (ys: [m]t) -> *[k]t
- Concatenation where the result has a predetermined size. If the provided size is wrong, the function will fail with a run-time error. 
- ↑val rotate [n] 't: (r: i64) -> (xs: [n]t) -> [n]t
- Rotate an array some number of elements to the left. A negative rotation amount is also supported. - For example, if - b==rotate r a, then- b[x] = a[x+r].- Complexity: O(1). 
- ↑val iota: (n: i64) -> *[n]i64
- Construct an array of consecutive integers of the given length, starting at 0. - Work: O(n). - Span: O(1). 
- ↑val indices [n] 't: [n]t -> *[n]i64
- Construct an array comprising valid indexes into some other array, starting at 0. - Work: O(n). - Span: O(1). 
- ↑val replicate 't: (n: i64) -> (x: t) -> *[n]t
- Construct an array of the given length containing the given value. - Work: O(n). - Span: O(1). 
- ↑val flatten [n] [m] 't: (xs: [n][m]t) -> []t
- Combines the outer two dimensions of an array. - Complexity: O(1). 
- ↑val flatten_to [n] [m] 't: (l: i64) -> (xs: [n][m]t) -> [l]t
- Like - flatten, but where the final size is known. Fails at runtime if the provided size is wrong.
- ↑val flatten_3d [n] [m] [l] 't: (xs: [n][m][l]t) -> []t
- Like - flatten, but on the outer three dimensions of an array.
- ↑val flatten_4d [n] [m] [l] [k] 't: (xs: [n][m][l][k]t) -> []t
- Like - flatten, but on the outer four dimensions of an array.
- ↑val unflatten [p] 't: (n: i64) -> (m: i64) -> (xs: [p]t) -> [n][m]t
- Splits the outer dimension of an array in two. - Complexity: O(1). 
- ↑val unflatten_3d [p] 't: (n: i64) -> (m: i64) -> (l: i64) -> (xs: [p]t) -> [n][m][l]t
- Like - unflatten, but produces three dimensions.
- ↑val unflatten_4d [p] 't: (n: i64) -> (m: i64) -> (l: i64) -> (k: i64) -> (xs: [p]t) -> [n][m][l][k]t
- Like - unflatten, but produces four dimensions.
- ↑val and [n]: (xs: [n]bool) -> bool
- True if all of the input elements are true. Produces true on an empty array. - Work: O(n). - Span: O(log(n)). 
- ↑val or [n]: (xs: [n]bool) -> bool
- True if any of the input elements are true. Produces false on an empty array. - Work: O(n). - Span: O(log(n)). 
- ↑val foldl [n] 'a 'b: (f: a -> b -> a) -> (acc: a) -> (bs: [n]b) -> a
- Perform a sequential left-fold of an array. - Work: O(n ✕ W(f))). - Span: O(n ✕ S(f)). 
- ↑val foldr [n] 'a 'b: (f: b -> a -> a) -> (acc: a) -> (bs: [n]b) -> a
- Perform a sequential right-fold of an array. - Work: O(n ✕ W(f))). - Span: O(n ✕ S(f)). 
- ↑val tabulate 'a: (n: i64) -> (f: i64 -> a) -> *[n]a
- Create a value for each point in a one-dimensional index space. - Work: O(n ✕ W(f)) - Span: O(S(f)) 
- ↑val tabulate_2d 'a: (n: i64) -> (m: i64) -> (f: i64 -> i64 -> a) -> *[n][m]a
- Create a value for each point in a two-dimensional index space. - Work: O(n ✕ W(f)) - Span: O(S(f)) 
- ↑val tabulate_3d 'a: (n: i64) -> (m: i64) -> (o: i64) -> (f: i64 -> i64 -> i64 -> a) -> *[n][m][o]a
- Create a value for each point in a three-dimensional index space. - Work: O(n ✕ W(f)) - Span: O(S(f))