## Definitions on Arrays #

This file contains various definitions on `Array`

. It does not contain
proofs about these definitions, those are contained in other files in `Std.Data.Array`

.

The array `#[0, 1, ..., n - 1]`

.

## Equations

- Array.range n = Nat.fold (flip Array.push) n #[]

Drop `none`

s from a Array, and replace each remaining `some a`

with `a`

.

## Equations

- Array.reduceOption l = Array.filterMap id l 0 (Array.size l)

Turns `#[#[a₁, a₂, ⋯], #[b₁, b₂, ⋯], ⋯]⋯], #[b₁, b₂, ⋯], ⋯]⋯], ⋯]⋯]`

into `#[a₁, a₂, ⋯, b₁, b₂, ⋯]⋯, b₁, b₂, ⋯]⋯]`

## Equations

- Array.flatten arr = Array.foldl (fun acc a => Array.append acc a) #[] arr 0 (Array.size arr)

Turns `#[a, b]`

into `#[(a, 0), (b, 1)]`

.

## Equations

- Array.zipWithIndex arr = Array.mapIdx arr fun i a => (a, i.val)

Check whether `xs`

and `ys`

are equal as sets, i.e. they contain the same
elements when disregarding order and duplicates. `O(n*m)`

! If your element type
has an `Ord`

instance, it is asymptotically more efficient to sort the two
arrays, remove duplicates and then compare them elementwise.

## Equations

- Array.equalSet xs ys = (Array.all xs (fun x => Array.contains ys x) 0 (Array.size xs) && Array.all ys (fun x => Array.contains xs x) 0 (Array.size ys))

Sort an array using `compare`

to compare elements.

## Equations

- Array.qsortOrd xs = Array.qsort xs (fun x y => Ordering.isLT (compare x y)) 0 (Array.size xs - 1)

Find the first minimal element of an array. If the array is empty, `d`

is
returned. If `start`

and `stop`

are given, only the subarray `xs[start:stop]`

is
considered.

## Equations

- Array.minD xs d start stop = Array.foldl (fun min x => if Ordering.isLT (compare x min) = true then x else min) d xs start stop

Find the first minimal element of an array. If the array is empty, `none`

is
returned. If `start`

and `stop`

are given, only the subarray `xs[start:stop]`

is
considered.

## Equations

- Array.min? xs start stop = if h : start < Array.size xs then some (Array.minD xs (Array.get xs { val := start, isLt := h }) start stop) else none

Find the first minimal element of an array. If the array is empty, `default`

is
returned. If `start`

and `stop`

are given, only the subarray `xs[start:stop]`

is
considered.

## Equations

- Array.minI xs start stop = Array.minD xs default start stop

Find the first maximal element of an array. If the array is empty, `d`

is
returned. If `start`

and `stop`

are given, only the subarray `xs[start:stop]`

is
considered.

## Equations

- Array.maxD xs d start stop = Array.minD xs d start stop

Find the first maximal element of an array. If the array is empty, `none`

is
returned. If `start`

and `stop`

are given, only the subarray `xs[start:stop]`

is
considered.

## Equations

- Array.max? xs start stop = Array.min? xs start stop

Find the first maximal element of an array. If the array is empty, `default`

is
returned. If `start`

and `stop`

are given, only the subarray `xs[start:stop]`

is
considered.

## Equations

- Array.maxI xs start stop = Array.minI xs start stop

The empty subarray.

## Equations

- Subarray.empty = { as := #[], start := 0, stop := 0, h₁ := Subarray.empty.proof_1, h₂ := Subarray.empty.proof_1 }

## Equations

- Subarray.instEmptyCollectionSubarray = { emptyCollection := Subarray.empty }

Check whether a subarray contains an element.

## Equations

- Subarray.contains as a = Subarray.any (fun x => x == a) as