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

Equations

• @Array.setN = @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]

Equations

• Array.scanlM f init as start stop = Array.scanlM.loop f init as (min start as.size) (min stop as.size) ⋯ #[]

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Array.scanrM f init as start stop = Array.scanrM.loop f init as (min start as.size) stop ⋯ #[]

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Array.scanl f init as start stop = (Array.scanlM (fun (x1 : β) (x2 : α) => pure (f x1 x2)) init as start stop).run

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

Equations

• Array.scanr f init as start stop = (Array.scanrM (fun (x1 : α) (x2 : β) => pure (f x1 x2)) init as start stop).run

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

Equations

• Subarray.scanlM f init as = Array.scanlM f init as.array as.start as.stop

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

Equations

• Subarray.scanrM f init as = Array.scanrM f init as.array as.start as.stop

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

Equations

• Subarray.scanl f init as = Array.scanl f init as.array as.start as.stop

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

Equations

• Subarray.scanr f init as = Array.scanr f init as.array as.start as.stop

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