Documentation

Std.Data.Array.Basic

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

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

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

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

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

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

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

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

Sort an array using compare to compare elements.

Equations
@[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
@[inline]
def Array.min? {α : Type u_1} [ord : Ord α] (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, none is returned. If start and stop are given, only the subarray xs[start:stop] is considered.

Equations
@[inline]
def Array.minI {α : Type u_1} [ord : Ord α] [inst : 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
@[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
@[inline]
def Array.max? {α : Type u_1} [ord : Ord α] (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, none is returned. If start and stop are given, only the subarray xs[start:stop] is considered.

Equations
@[inline]
def Array.maxI {α : Type u_1} [ord : Ord α] [inst : 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
def Subarray.empty {α : Type u_1} :

The empty subarray.

Equations
Equations
  • Subarray.instEmptyCollectionSubarray = { emptyCollection := Subarray.empty }
Equations
  • Subarray.instInhabitedSubarray = { default := }
@[inline]
def Subarray.isEmpty {α : Type u_1} (as : Subarray α) :

Check whether a subarray is empty.

Equations
@[inline]
def Subarray.contains {α : Type u_1} [inst : BEq α] (as : Subarray α) (a : α) :

Check whether a subarray contains an element.

Equations
def Subarray.popHead? {α : Type u_1} (as : 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.