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.

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

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

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

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

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

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

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

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

@[deprecated Array.set (since := "2026-02-02")]

def Array.setN {α : Type u_1} (xs : Array α) (i : Nat) (v : α) (h : i < xs.size := by get_elem_tactic) : Array α

Alias of Array.set.

@[implemented_by _private.Batteries.Data.Array.Basic.0.Array.scanlMFast]

def Array.scanlM {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [Monad m] (f : β → α → m β) (init : β) (as : Array α) (start : Nat := 0) (stop : Nat := as.size) : m (Array β)

Folds a monadic function over an array from the left, accumulating the partial results starting with init. The accumulated value is combined with the each element of the list in order, using f.

The optional parameters start and stop control the region of the array to be folded. Folding proceeds from start (inclusive) to stop (exclusive), so no folding occurs unless start < stop. By default, the entire array is folded.

Examples:

example [Monad m] (f : α → β → m α) :
    Array.scanlM f x₀ #[a, b, c] = (do
      let x₁ ← f x₀ a
      let x₂ ← f x₁ b
      let x₃ ← f x₂ c
      pure #[x₀, x₁, x₂, x₃])
    := by simp [scanlM, scanlM.loop]

example [Monad m] (f : α → β → m α) :
    Array.scanlM f x₀ #[a, b, c] (start := 1) (stop := 3) = (do
      let x₁ ← f x₀ b
      let x₂ ← f x₁ c
      pure #[x₀, x₁, x₂])
    := by simp [scanlM, scanlM.loop]

@[irreducible]

def Array.scanlM.loop {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [Monad m] (f : β → α → m β) (init : β) (as : Array α) (start stop : Nat) (h_stop : stop ≤ as.size) (acc : Array β) : m (Array β)

auxiliary tail-recursive function for scanlM

@[implemented_by _private.Batteries.Data.Array.Basic.0.Array.scanrMUnsafe]

def Array.scanrM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → β → m β) (init : β) (as : Array α) (start : Nat := as.size) (stop : Nat := 0) : m (Array β)

Folds a monadic function over an array from the right, accumulating the partial results starting with init. The accumulated value is combined with the each element of the list in order using f.

The optional parameters start and stop control the region of the array to be folded. Folding proceeds from start (exclusive) to stop (inclusive), so no folding occurs unless start > stop. By default, the entire array is folded.

Examples:

example [Monad m] (f : α → β → m β) :
    Array.scanrM f x₀ #[a, b, c] = (do
      let x₁ ← f c x₀
      let x₂ ← f b x₁
      let x₃ ← f a x₂
      pure #[x₃, x₂, x₁, x₀])
    := by simp [scanrM, scanrM.loop]

example [Monad m] (f : α → β → m β) :
    Array.scanrM f x₀ #[a, b, c] (start := 3) (stop := 1) = (do
      let x₁ ← f c x₀
      let x₂ ← f b x₁
      pure #[x₂, x₁, x₀])
    := by simp [scanrM, scanrM.loop]

@[irreducible]

def Array.scanrM.loop {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → β → m β) (init : β) (as : Array α) (start stop : Nat) (h_start : start ≤ as.size) (acc : Array β) : m (Array β)

auxiliary tail-recursive function for scanrM

@[inline]

def Array.scanl {β : Type u_1} {α : Type u_2} (f : β → α → β) (init : β) (as : Array α) (start : Nat := 0) (stop : Nat := as.size) : Array β

Fold a function f over the array from the left, returning the array of partial results.

scanl (· + ·) 0 #[1, 2, 3] = #[0, 1, 3, 6]

@[inline]

def Array.scanr {α : Type u_1} {β : Type u_2} (f : α → β → β) (init : β) (as : Array α) (start : Nat := as.size) (stop : Nat := 0) : Array β

Fold a function f over the array from the right, returning the array of partial results.

scanr (· + ·) 0 #[1, 2, 3] = #[6, 5, 3, 0]

@[inline]

def Subarray.scanlM {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [Monad m] (f : β → α → m β) (init : β) (as : Subarray α) : m (Array β)

Fold a monadic function f over the subarray from the left, returning the list of partial results.

@[inline]

def Subarray.scanrM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → β → m β) (init : β) (as : Subarray α) : m (Array β)

Fold a monadic function f over the subarray from the right, returning the list of partial results.

@[inline]

def Subarray.scanl {β : Type u_1} {α : Type u_2} (f : β → α → β) (init : β) (as : Subarray α) : Array β

Fold a function f over the subarray from the left, returning the list of partial results.

@[inline]

def Subarray.scanr {α : Type u_1} {β : Type u_2} (f : α → β → β) (init : β) (as : Subarray α) : Array β

Fold a function f over the subarray from the right, returning the list of partial results.

@[inline]

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

Check whether a subarray is empty.

@[inline]

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

Check whether a subarray contains a given element.

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.