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.

def Array.range (n : Nat) : Array Nat

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

Equations

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

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

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

Equations

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

def Array.flatten {α : Type u_1} (arr : Array (Array α)) : Array α

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

Equations

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

def Array.zipWithIndex {α : Type u_1} (arr : Array α) : Array (α × Nat)

Turns #[a, b] into #[(a, 0), (b, 1)].

Equations

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

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

• 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))

def Array.qsortOrd {α : Type u_1} [ord : Ord α] (xs : Array α) : Array α

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)

@[inline]

def Array.minD {α : Type u_1} [ord : Ord α] (xs : Array α) (d : α) (start : optParam Nat 0) (stop : optParam Nat (Array.size xs)) : α

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

@[inline]

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

• 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

@[inline]

def Array.minI {α : Type u_1} [ord : Ord α] [Inhabited α] (xs : Array α) (start : optParam Nat 0) (stop : optParam Nat (Array.size xs)) : α

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

@[inline]

def Array.maxD {α : Type u_1} [ord : Ord α] (xs : Array α) (d : α) (start : optParam Nat 0) (stop : optParam Nat (Array.size xs)) : α

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

@[inline]

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

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

@[inline]

def Array.maxI {α : Type u_1} [ord : Ord α] [Inhabited α] (xs : Array α) (start : optParam Nat 0) (stop : optParam Nat (Array.size xs)) : α

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

def Subarray.empty {α : Type u_1} : Subarray α

The empty subarray.

Equations

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

instance Subarray.instEmptyCollectionSubarray {α : Type u_1} : EmptyCollection (Subarray α)

Equations

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

instance Subarray.instInhabitedSubarray {α : Type u_1} : Inhabited (Subarray α)

Equations

• Subarray.instInhabitedSubarray = { default := ∅ }

@[inline]

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

Check whether a subarray is empty.

Equations

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

@[inline]

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

Check whether a subarray contains an element.

Equations

• Subarray.contains as 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.