## Abstract

Utility functions for arrays.

## Synopsis

open import "prelude/zip" | ||

val length | [n] t : | [n]t -> i32 |

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) -> []t |

val init | [n] t : | (x: [n]t) -> []t |

val take | [n] t : | (i: i32) -> (x: [n]t) -> [i]t |

val drop | [n] t : | (i: i32) -> (x: [n]t) -> []t |

val split | [n] t : | (i: i32) -> (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: i32) -> (xs: [n]t) -> (ys: [m]t) -> *[k]t |

val rotate | [n] t : | (r: i32) -> (xs: [n]t) -> [n]t |

val iota | : | (n: i32) -> *[n]i32 |

val indices | [n] t : | [n]t -> *[n]i32 |

val replicate | t : | (n: i32) -> (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: i32) -> (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: i32) -> (m: i32) -> (xs: [p]t) -> [n][m]t |

val unflatten_3d | [p] t : | (n: i32) -> (m: i32) -> (l: i32) -> (xs: [p]t) -> [n][m][l]t |

val unflatten_4d | [p] t : | (n: i32) -> (m: i32) -> (l: i32) -> (k: i32) -> (xs: [p]t) -> [n][m][l][k]t |

val transpose | [n] [m] t : | (a: [n][m]t) -> [m][n]t |

val and | [funret₀] : | []bool -> bool |

val or | [funret₀] : | []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: i32) -> (f: i32 -> a) -> *[n]a |

val tabulate_2d | a : | (n: i32) -> (m: i32) -> (f: i32 -> i32 -> a) -> *[n][m]a |

val tabulate_3d | a : | (n: i32) -> (m: i32) -> (o: i32) -> (f: i32 -> i32 -> i32 -> a) -> *[n][m][o]a |

## Description

- ↑val take [n] t: (i: i32) -> (x: [n]t) -> [i]t
Take some number of elements from the head of the array.

- ↑val drop [n] t: (i: i32) -> (x: [n]t) -> []t
Remove some number of elements from the head of the array.

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

- ↑val concat_to [n] [m] t: (k: i32) -> (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: i32) -> (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+r] = a[x]`

.- ↑val iota: (n: i32) -> *[n]i32
Construct an array of consecutive integers of the given length, starting at 0.

- ↑val indices [n] t: [n]t -> *[n]i32
Construct an array comprising valid indexes into some other array, starting at 0.

- ↑val replicate t: (n: i32) -> (x: t) -> *[n]t
Construct an array of the given length containing the given value.

- ↑val flatten_to [n] [m] t: (l: i32) -> (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
Combines the outer three dimensions of an array.

- ↑val flatten_4d [n] [m] [l] [k] t: (xs: [n][m][l][k]t) -> []t
Combines the outer four dimensions of an array.

- ↑val unflatten [p] t: (n: i32) -> (m: i32) -> (xs: [p]t) -> [n][m]t
Splits the outer dimension of an array in two.

- ↑val unflatten_3d [p] t: (n: i32) -> (m: i32) -> (l: i32) -> (xs: [p]t) -> [n][m][l]t
Splits the outer dimension of an array in three.

- ↑val unflatten_4d [p] t: (n: i32) -> (m: i32) -> (l: i32) -> (k: i32) -> (xs: [p]t) -> [n][m][l][k]t
Splits the outer dimension of an array in four.

- ↑val and [funret₀]: []bool -> bool
True if all of the input elements are true. Produces true on an empty array.

- ↑val or [funret₀]: []bool -> bool
True if any of the input elements are true. Produces false on an empty array.

- ↑val foldl [n] a b: (f: a -> b -> a) -> (acc: a) -> (bs: [n]b) -> a
Perform a

*sequential*left-fold of an array.- ↑val foldr [n] a b: (f: b -> a -> a) -> (acc: a) -> (bs: [n]b) -> a
Perform a

*sequential*right-fold of an array.- ↑val tabulate a: (n: i32) -> (f: i32 -> a) -> *[n]a
Create a value for each point in a one-dimensional index space.

- ↑val tabulate_2d a: (n: i32) -> (m: i32) -> (f: i32 -> i32 -> a) -> *[n][m]a
Create a value for each point in a two-dimensional index space.

- ↑val tabulate_3d a: (n: i32) -> (m: i32) -> (o: i32) -> (f: i32 -> i32 -> i32 -> a) -> *[n][m][o]a
Create a value for each point in a three-dimensional index space.