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.reduceOption {α : Type u_1} (l : Array (Option α)) : Array α

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

Equations

• l.reduceOption = Array.filterMap id l 0

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

• xs.equalSet ys = (xs.all (fun (x : α) => ys.contains x) 0 && ys.all (fun (x : α) => xs.contains x) 0)

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

Sort an array using compare to compare elements.

Equations

• xs.qsortOrd = xs.qsort (fun (x y : α) => (compare x y).isLT) 0

@[inline]

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

@[inline]

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

@[inline]

def Array.min? {α : Type u_1} [ord : Ord α] (xs : Array α) (start : optParam Nat 0) (stop : optParam 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.get ⟨start, ⋯⟩) start stop) else none

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[implemented_by _private.Std.Data.Array.Basic.0.Array.attachWithImpl]

def Array.attachWith {α : Type u_1} (xs : Array α) (P : α → Prop) (H : ∀ (x : α), x ∈ xs → P 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 ⋯ }

@[inline]

def Array.attach {α : Type u_1} (xs : Array α) : 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) ⋯

@[inline]

def Array.join {α : Type u_1} (l : Array (Array α)) : 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

• l.join = Array.foldl (fun (x x_1 : Array α) => x ++ x_1) #[] l 0

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

The empty subarray.

Equations

• Subarray.empty = { array := #[], start := 0, stop := 0, start_le_stop := Subarray.empty.proof_1, stop_le_array_size := Subarray.empty.proof_1 }

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

Equations

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

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

Equations

• Subarray.instInhabited_std = { default := ∅ }

@[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.