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.equalSet {α : Type u_1} [BEq α] (xs ys : Array α) : Bool

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) && ys.all fun (x : α) => xs.contains x)

@[inline]

def Array.minWith {α : Type u_1} [ord : Ord α] (xs : Array α) (d : α) (start : Nat := 0) (stop : 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

@[inline]

def Array.minD {α : Type u_1} [ord : Ord α] (xs : Array α) (d : α) (start : Nat := 0) (stop : 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[start] (start + 1) stop else d

@[inline]

def Array.min? {α : Type u_1} [ord : Ord α] (xs : Array α) (start : Nat := 0) (stop : Nat := xs.size) : Option α

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[start] start stop) else none

@[inline]

def Array.minI {α : Type u_1} [ord : Ord α] [Inhabited α] (xs : Array α) (start : Nat := 0) (stop : 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

@[inline]

def Array.maxWith {α : Type u_1} [ord : Ord α] (xs : Array α) (d : α) (start : Nat := 0) (stop : 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

@[inline]

def Array.maxD {α : Type u_1} [ord : Ord α] (xs : Array α) (d : α) (start : Nat := 0) (stop : 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

@[inline]

def Array.max? {α : Type u_1} [ord : Ord α] (xs : Array α) (start : Nat := 0) (stop : Nat := xs.size) : Option α

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

@[inline]

def Array.maxI {α : Type u_1} [ord : Ord α] [Inhabited α] (xs : Array α) (start : Nat := 0) (stop : 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

@[deprecated Array.flatten (since := "2024-10-15")]

def Array.join {α : Type u} (xss : Array (Array α)) : Array α

Alias of Array.flatten.

---

Appends the contents of array of arrays into a single array. The resulting array contains the same elements as the nested arrays in the same order.

Examples:

• #[#[5], #[4], #[3, 2]].flatten = #[5, 4, 3, 2]
• #[#[0, 1], #[], #[2], #[1, 0, 1]].flatten = #[0, 1, 2, 1, 0, 1]
• (#[] : Array Nat).flatten = #[]

Equations

• @Array.join = @Array.flatten

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.

@[reducible, inline]

abbrev Array.setN {α : Type u_1} (a : Array α) (i : Nat) (x : α) (h : i < a.size := by get_elem_tactic) : Array α

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 x h = a.set i x h

@[deprecated Array.swap (since := "2024-11-24")]

def Array.swapN {α : Type u} (xs : Array α) (i j : Nat) (hi : i < xs.size := by get_elem_tactic) (hj : j < xs.size := by get_elem_tactic) : Array α

Alias of Array.swap.

---

Swaps two elements of an array. The modification is performed in-place when the reference to the array is unique.

Examples:

• #["red", "green", "blue", "brown"].swap 0 3 = #["brown", "green", "blue", "red"]
• #["red", "green", "blue", "brown"].swap 0 2 = #["blue", "green", "red", "brown"]
• #["red", "green", "blue", "brown"].swap 1 2 = #["red", "blue", "green", "brown"]
• #["red", "green", "blue", "brown"].swap 3 0 = #["brown", "green", "blue", "red"]

Equations

• @Array.swapN = @Array.swap

@[deprecated Array.swapAt (since := "2024-11-24")]

def Array.swapAtN {α : Type u} (xs : Array α) (i : Nat) (v : α) (hi : i < xs.size := by get_elem_tactic) : α × Array α

Alias of Array.swapAt.

---

Swaps a new element with the element at the given index.

Returns the value formerly found at i, paired with an array in which the value at i has been replaced with v.

Examples:

• #["spinach", "broccoli", "carrot"].swapAt 1 "pepper" = ("broccoli", #["spinach", "pepper", "carrot"])
• #["spinach", "broccoli", "carrot"].swapAt 2 "pepper" = ("carrot", #["spinach", "broccoli", "pepper"])

Equations

• @Array.swapAtN = @Array.swapAt

@[deprecated Array.eraseIdx (since := "2024-11-20")]

def Array.eraseIdxN {α : Type u} (xs : Array α) (i : Nat) (h : i < xs.size := by get_elem_tactic) : Array α

Alias of Array.eraseIdx.

---

Removes the element at a given index from an array without a run-time bounds check.

This function takes worst-case O(n) time because it back-shifts all elements at positions greater than i.

Examples:

• #["apple", "pear", "orange"].eraseIdx 0 = #["pear", "orange"]
• #["apple", "pear", "orange"].eraseIdx 1 = #["apple", "orange"]
• #["apple", "pear", "orange"].eraseIdx 2 = #["apple", "pear"]

Equations

• @Array.eraseIdxN = @Array.eraseIdx

@[inline]

def Subarray.isEmpty {α : Type u_1} (as : Subarray α) : Bool

Check whether a subarray is empty.

Equations

• as.isEmpty = (as.start == as.stop)

@[inline]

def Subarray.contains {α : Type u_1} [BEq α] (as : Subarray α) (a : α) : Bool

Check whether a subarray contains an element.

Equations

• as.contains a = Subarray.any (fun (x : α) => x == a) as

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

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.