# Documentation

## 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 Batteries.Data.Array.

def Array.reduceOption {α : Type u_1} (l : Array ()) :

Drop nones from a Array, and replace each remaining some a with a.

Equations
Instances For
def Array.equalSet {α : Type u_1} [BEq α] (xs : ) (ys : ) :

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
• xs.equalSet ys = (xs.all (fun (x : α) => ys.contains x) 0 && ys.all (fun (x : α) => xs.contains x) 0)
Instances For
def Array.qsortOrd {α : Type u_1} [ord : Ord α] (xs : ) :

Sort an array using compare to compare elements.

Equations
• xs.qsortOrd = xs.qsort (fun (x y : α) => (compare x y).isLT) 0
Instances For
@[inline]
def Array.minWith {α : Type u_1} [ord : Ord α] (xs : ) (d : α) (start : ) (stop : optParam Nat xs.size) :
α

Returns the first minimal element among d and elements of the array. If start and stop are given, only the subarray xs[start:stop] is considered (in addition to d).

Equations
• xs.minWith d start stop = Array.foldl (fun (min x : α) => if (compare x min).isLT = true then x else min) d xs start stop
Instances For
@[inline]
def Array.minD {α : Type u_1} [ord : Ord α] (xs : ) (d : α) (start : ) (stop : optParam Nat xs.size) :
α

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
• xs.minD d start stop = if h : start < xs.size start < stop then xs.minWith (xs.get start, ) (start + 1) stop else d
Instances For
@[inline]
def Array.min? {α : Type u_1} [ord : Ord α] (xs : ) (start : ) (stop : optParam Nat xs.size) :

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
• xs.min? start stop = if h : start < xs.size start < stop then some (xs.minD (xs.get start, ) start stop) else none
Instances For
@[inline]
def Array.minI {α : Type u_1} [ord : Ord α] [] (xs : ) (start : ) (stop : optParam Nat xs.size) :
α

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
• xs.minI start stop = xs.minD default start stop
Instances For
@[inline]
def Array.maxWith {α : Type u_1} [ord : Ord α] (xs : ) (d : α) (start : ) (stop : optParam Nat xs.size) :
α

Returns the first maximal element among d and elements of the array. If start and stop are given, only the subarray xs[start:stop] is considered (in addition to d).

Equations
• xs.maxWith d start stop = xs.minWith d start stop
Instances For
@[inline]
def Array.maxD {α : Type u_1} [ord : Ord α] (xs : ) (d : α) (start : ) (stop : optParam Nat xs.size) :
α

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
• xs.maxD d start stop = xs.minD d start stop
Instances For
@[inline]
def Array.max? {α : Type u_1} [ord : Ord α] (xs : ) (start : ) (stop : optParam Nat xs.size) :

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
• xs.max? start stop = xs.min? start stop
Instances For
@[inline]
def Array.maxI {α : Type u_1} [ord : Ord α] [] (xs : ) (start : ) (stop : optParam Nat xs.size) :
α

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
• xs.maxI start stop = xs.minI start stop
Instances For
@[implemented_by _private.Batteries.Data.Array.Basic.0.Array.attachWithImpl]
def Array.attachWith {α : Type u_1} (xs : ) (P : αProp) (H : ∀ (x : α), x xsP x) :
Array { x : α // P x }

O(1). "Attach" a proof P x that holds for all the elements of xs to produce a new array with the same elements but in the type {x // P x}.

Equations
• xs.attachWith P H = { data := xs.data.attachWith P }
Instances For
@[inline]
def Array.attach {α : Type u_1} (xs : ) :
Array { x : α // x xs }

O(1). "Attach" the proof that the elements of xs are in xs to produce a new array with the same elements but in the type {x // x ∈ xs}.

Equations
• xs.attach = xs.attachWith (fun (x : α) => x xs)
Instances For
@[inline]
def Array.join {α : Type u_1} (l : Array ()) :

O(|join L|). join L concatenates all the arrays in L into one array.

• join #[#[a], #[], #[b, c], #[d, e, f]] = #[a, b, c, d, e, f]
Equations
Instances For

### Safe Nat Indexed Array functions #

The functions in this section offer variants of Array functions which use Nat indices instead of Fin indices. All these functions have as parameter a proof that the index is valid for the array. But this parameter has a default argument by get_elem_tactic which should prove the index bound.

def Array.setN {α : Type u_1} (a : ) (i : Nat) (h : autoParam (i < a.size) _auto✝) (x : α) :

setN a i h x sets an element in a vector using a Nat index which is provably valid. A proof by get_elem_tactic is provided as a default argument for h. This will perform the update destructively provided that a has a reference count of 1 when called.

Equations
• a.setN i h x = a.set i, h x
Instances For
def Array.swapN {α : Type u_1} (a : ) (i : Nat) (j : Nat) (hi : autoParam (i < a.size) _auto✝) (hj : autoParam (j < a.size) _auto✝) :

swapN a i j hi hj swaps two Nat indexed entries in an Array α. Uses get_elem_tactic to supply a proof that the indices are in range. hi and hj are both given a default argument by get_elem_tactic. This will perform the update destructively provided that a has a reference count of 1 when called.

Equations
• a.swapN i j hi hj = a.swap i, hi j, hj
Instances For
def Array.swapAtN {α : Type u_1} (a : ) (i : Nat) (h : autoParam (i < a.size) _auto✝) (x : α) :
α ×

swapAtN a i h x swaps the entry with index i : Nat in the vector for a new entry x. The old entry is returned alongwith the modified vector. Automatically generates proof of i < a.size with get_elem_tactic where feasible.

Equations
• a.swapAtN i h x = a.swapAt i, h x
Instances For
def Array.eraseIdxN {α : Type u_1} (a : ) (i : Nat) (h : autoParam (i < a.size) _auto✝) :

eraseIdxN a i h Removes the element at position i from a vector of length n. h : i < a.size has a default argument by get_elem_tactic which tries to supply a proof that the index is valid. This function takes worst case O(n) time because it has to backshift all elements at positions greater than i.

Equations
• a.eraseIdxN i h = a.feraseIdx i, h
Instances For
def Subarray.empty {α : Type u_1} :

The empty subarray.

Equations
Instances For
Equations
• Subarray.instEmptyCollection_batteries = { emptyCollection := Subarray.empty }
Equations
• Subarray.instInhabited_batteries = { default := }
@[inline]
def Subarray.isEmpty {α : Type u_1} (as : ) :

Check whether a subarray is empty.

Equations
• as.isEmpty = (as.start == as.stop)
Instances For
@[inline]
def Subarray.contains {α : Type u_1} [BEq α] (as : ) (a : α) :

Check whether a subarray contains an element.

Equations
Instances For
def Subarray.popHead? {α : Type u_1} (as : ) :
Option (α × )

Remove the first element of a subarray. Returns the element and the remaining subarray, or none if the subarray is empty.

Equations
• One or more equations did not get rendered due to their size.
Instances For