Documentation

theorem Array.ext' {α : Type u} {xs ys : Array α} (h : xs.toList = ys.toList) :

xs = ys

@[simp]

theorem Array.toArrayAux_eq {α : Type u} (as : List α) (acc : Array α) :

(as.toArrayAux acc).toList = acc.toList ++ as

@[simp]

theorem Array.toArray_toList {α : Type u} (xs : Array α) :

xs.toList.toArray = xs

@[simp]

theorem Array.getElem_toList {α : Type u} {xs : Array α} {i : Nat} (h : i < xs.size) :

xs.toList[i] = xs[i]

@[simp]

theorem Array.getElem?_toList {α : Type u} {xs : Array α} {i : Nat} :

xs.toList[i]? = xs[i]?

structure Array.Mem {α : Type u} (as : Array α) (a : α) :

Prop

a ∈ as is a predicate which asserts that a is in the array as.

val : a ∈ as.toList

instance Array.instMembership {α : Type u} :

Membership α (Array α)

Equations

Array.instMembership = { mem := Array.Mem }

theorem Array.mem_def {α : Type u} {a : α} {as : Array α} :

a ∈ as ↔ a ∈ as.toList

@[simp]

theorem Array.mem_toArray {α : Type u} {a : α} {l : List α} :

a ∈ l.toArray ↔ a ∈ l

@[simp]

theorem Array.getElem_mem {α : Type u} {xs : Array α} {i : Nat} (h : i < xs.size) :

xs[i] ∈ xs

@[reducible, inline, deprecated Array.toArray_toList (since := "2025-02-17")]

abbrev List.toArray_toList {α : Type u_1} (xs : Array α) :

xs.toList.toArray = xs

Equations

@List.toArray_toList = @Array.toArray_toList

theorem List.toList_toArray {α : Type u} (as : List α) :

as.toArray.toList = as

@[reducible, inline, deprecated List.toList_toArray (since := "2025-02-17")]

abbrev Array.toList_toArray {α : Type u_1} (as : List α) :

as.toArray.toList = as

Equations

@Array.toList_toArray = @List.toList_toArray

@[simp]

theorem List.size_toArray {α : Type u} (as : List α) :

as.toArray.size = as.length

@[reducible, inline, deprecated List.size_toArray (since := "2025-02-17")]

abbrev Array.size_toArray {α : Type u_1} (as : List α) :

as.toArray.size = as.length

Equations

@Array.size_toArray = @List.size_toArray

@[simp]

theorem List.getElem_toArray {α : Type u} {xs : List α} {i : Nat} (h : i < xs.toArray.size) :

xs.toArray[i] = xs[i]

@[simp]

theorem List.getElem?_toArray {α : Type u} {xs : List α} {i : Nat} :

xs.toArray[i]? = xs[i]?

@[simp]

theorem List.getElem!_toArray {α : Type u} [Inhabited α] {xs : List α} {i : Nat} :

xs.toArray[i]! = xs[i]!

theorem Array.size_eq_length_toList {α : Type u} (xs : Array α) :

xs.size = xs.toList.length

@[reducible, inline, deprecated Array.toList_toArray (since := "2024-09-09")]

abbrev Array.data_toArray {α : Type u_1} (as : List α) :

as.toArray.toList = as

Equations

@Array.data_toArray = @List.toList_toArray

@[reducible, inline, deprecated Array.toList (since := "2024-09-10")]

abbrev Array.Array.data {α : Type u_1} (self : Array α) :

List α

Equations

@Array.Array.data = @Array.toList

Externs #

@[extern lean_array_size]

def Array.usize {α : Type u} (a : Array α) :

USize

Low-level version of size that directly queries the C array object cached size. While this is not provable, usize always returns the exact size of the array since the implementation only supports arrays of size less than USize.size.

Equations

a.usize = a.size.toUSize

@[extern lean_array_uget]

def Array.uget {α : Type u} (a : Array α) (i : USize) (h : i.toNat < a.size) :

Low-level version of fget which is as fast as a C array read. Fin values are represented as tag pointers in the Lean runtime. Thus, fget may be slightly slower than uget.

Equations

a.uget i h = a[i.toNat]

@[extern lean_array_uset]

def Array.uset {α : Type u} (xs : Array α) (i : USize) (v : α) (h : i.toNat < xs.size) :

Array α

Low-level version of fset which is as fast as a C array fset. Fin values are represented as tag pointers in the Lean runtime. Thus, fset may be slightly slower than uset.

Equations

xs.uset i v h = xs.set i.toNat v h

@[extern lean_array_pop]

def Array.pop {α : Type u} (xs : Array α) :

Array α

Equations

xs.pop = { toList := xs.toList.dropLast }

@[simp]

theorem Array.size_pop {α : Type u} (xs : Array α) :

xs.pop.size = xs.size - 1

@[extern lean_mk_array]

def Array.mkArray {α : Type u} (n : Nat) (v : α) :

Array α

Equations

mkArray n v = { toList := List.replicate n v }

@[extern lean_array_fswap]

def Array.swap {α : Type u} (xs : Array α) (i j : Nat) (hi : i < xs.size := by get_elem_tactic) (hj : j < xs.size := by get_elem_tactic) :

Array α

Swaps two entries in an array.

This will perform the update destructively provided that a has a reference count of 1 when called.

Equations

xs.swap i j hi hj = (xs.set i xs[j] hi).set j xs[i] ⋯

@[simp]

theorem Array.size_swap {α : Type u} (xs : Array α) (i j : Nat) {hi : i < xs.size} {hj : j < xs.size} :

(xs.swap i j hi hj).size = xs.size

@[extern lean_array_swap]

def Array.swapIfInBounds {α : Type u} (xs : Array α) (i j : Nat) :

Array α

Swaps two entries in an array, or returns the array unchanged if either index is out of bounds.

This will perform the update destructively provided that a has a reference count of 1 when called.

Equations

xs.swapIfInBounds i j = if h₁ : i < xs.size then if h₂ : j < xs.size then xs.swap i j h₁ h₂ else xs else xs

@[reducible, inline, deprecated Array.swapIfInBounds (since := "2024-11-24")]

abbrev Array.swap! {α : Type u_1} (xs : Array α) (i j : Nat) :

Array α

Equations

@Array.swap! = @Array.swapIfInBounds

GetElem instance for `USize`, backed by `uget` #

instance Array.instGetElemUSizeLtNatToNatSize {α : Type u} :

GetElem (Array α) USize α fun (xs : Array α) (i : USize) => i.toNat < xs.size

Equations

Array.instGetElemUSizeLtNatToNatSize = { getElem := fun (xs : Array α) (i : USize) (h : i.toNat < xs.size) => xs.uget i h }

Definitions #

instance Array.instEmptyCollection {α : Type u} :

EmptyCollection (Array α)

Equations

Array.instEmptyCollection = { emptyCollection := #[] }

instance Array.instInhabited {α : Type u} :

Inhabited (Array α)

Equations

Array.instInhabited = { default := #[] }

def Array.isEmpty {α : Type u} (xs : Array α) :

Equations

xs.isEmpty = decide (xs.size = 0)

@[specialize #[]]

def Array.isEqvAux {α : Type u} (xs ys : Array α) (hsz : xs.size = ys.size) (p : α → α → Bool) (i : Nat) :

i ≤ xs.size → Bool

Equations

xs.isEqvAux ys hsz p 0 x_2 = true
xs.isEqvAux ys hsz p i.succ h = (p xs[i] ys[i] && xs.isEqvAux ys hsz p i ⋯)

@[inline]

def Array.isEqv {α : Type u} (xs ys : Array α) (p : α → α → Bool) :

Equations

xs.isEqv ys p = if h : xs.size = ys.size then xs.isEqvAux ys h p xs.size ⋯ else false

instance Array.instBEq {α : Type u} [BEq α] :

BEq (Array α)

Equations

Array.instBEq = { beq := fun (xs ys : Array α) => xs.isEqv ys BEq.beq }

def Array.ofFn {α : Type u} {n : Nat} (f : Fin n → α) :

Array α

ofFn f with f : Fin n → α returns the list whose ith element is f i.

ofFn f = #[f 0, f 1, ... , f(n - 1)]

Equations

Array.ofFn f = Array.ofFn.go f 0 (Array.mkEmpty n)

def Array.ofFn.go {α : Type u} {n : Nat} (f : Fin n → α) (i : Nat) (acc : Array α) :

Array α

Auxiliary for ofFn. ofFn.go f i acc = acc ++ #[f i, ..., f(n - 1)]

Equations

Array.ofFn.go f i acc = if h : i < n then Array.ofFn.go f (i + 1) (acc.push (f ⟨i, h⟩)) else acc

def Array.range (n : Nat) :

Array Nat

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

Equations

Array.range n = Array.ofFn fun (i : Fin n) => ↑i

def Array.range' (start size : Nat) (step : Nat := 1) :

Array Nat

The array #[start, start + step, ..., start + step * (size - 1)].

Equations

Array.range' start size step = Array.ofFn fun (i : Fin size) => start + step * ↑i

@[inline]

def Array.singleton {α : Type u} (v : α) :

Array α

Equations

Array.singleton v = #[v]

def Array.back! {α : Type u} [Inhabited α] (xs : Array α) :

Return the last element of an array, or panic if the array is empty.

See back for the version that requires a proof the array is non-empty, or back? for the version that returns an option.

Equations

xs.back! = xs[xs.size - 1]!

def Array.back {α : Type u} (xs : Array α) (h : 0 < xs.size := by get_elem_tactic) :

Return the last element of an array, given a proof that the array is not empty.

See back! for the version that panics if the array is empty, or back? for the version that returns an option.

Equations

xs.back h = xs[xs.size - 1]

def Array.back? {α : Type u} (xs : Array α) :

Option α

Return the last element of an array, or none if the array is empty.

See back! for the version that panics if the array is empty, or back for the version that requires a proof the array is non-empty.

Equations

xs.back? = xs[xs.size - 1]?

@[deprecated "Use `a[i]?` instead." (since := "2025-02-12")]

def Array.get? {α : Type u} (xs : Array α) (i : Nat) :

Option α

Equations

xs.get? i = if h : i < xs.size then some xs[i] else none

@[inline]

def Array.swapAt {α : Type u} (xs : Array α) (i : Nat) (v : α) (hi : i < xs.size := by get_elem_tactic) :

α × Array α

Equations

xs.swapAt i v hi = (xs[i], xs.set i v hi)

@[inline]

def Array.swapAt! {α : Type u} (xs : Array α) (i : Nat) (v : α) :

α × Array α

Equations

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

def Array.shrink {α : Type u} (xs : Array α) (n : Nat) :

Array α

shrink a n returns the first n elements of a, implemented by repeatedly popping the last element.

Equations

xs.shrink n = Array.shrink.loop (xs.size - n) xs

def Array.shrink.loop {α : Type u} :

Nat → Array α → Array α

Equations

Array.shrink.loop 0 x✝ = x✝
Array.shrink.loop n.succ x✝ = Array.shrink.loop n x✝.pop

@[reducible, inline]

abbrev Array.take {α : Type u} (xs : Array α) (i : Nat) :

Array α

take a n returns the first n elements of a, implemented by copying the first n elements.

Equations

xs.take i = xs.extract 0 i

@[simp]

theorem Array.take_eq_extract {α : Type u} (xs : Array α) (i : Nat) :

xs.take i = xs.extract 0 i

@[reducible, inline]

abbrev Array.drop {α : Type u} (xs : Array α) (i : Nat) :

Array α

drop a n removes the first n elements of a, implemented by copying the remaining elements.

Equations

xs.drop i = xs.extract i

@[simp]

theorem Array.drop_eq_extract {α : Type u} (xs : Array α) (i : Nat) :

xs.drop i = xs.extract i

@[inline]

unsafe def Array.modifyMUnsafe {α : Type u} {m : Type u → Type u_1} [Monad m] (xs : Array α) (i : Nat) (f : α → m α) :

m (Array α)

Equations

xs.modifyMUnsafe i f = if h : i < xs.size then let v := xs[i]; let xs' := xs.set i (unsafeCast ()) h; do let v ← f v pure (xs'.set i v ⋯) else pure xs

@[implemented_by Array.modifyMUnsafe]

def Array.modifyM {α : Type u} {m : Type u → Type u_1} [Monad m] (xs : Array α) (i : Nat) (f : α → m α) :

m (Array α)

Equations

xs.modifyM i f = if h : i < xs.size then let v := xs[i]; do let v ← f v pure (xs.set i v h) else pure xs

@[inline]

def Array.modify {α : Type u} (xs : Array α) (i : Nat) (f : α → α) :

Array α

Equations

xs.modify i f = (xs.modifyM i f).run

@[inline]

def Array.modifyOp {α : Type u} (xs : Array α) (idx : Nat) (f : α → α) :

Array α

Equations

xs.modifyOp idx f = xs.modify idx f

@[inline]

unsafe def Array.forIn'Unsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (b : β) (f : (a : α) → a ∈ as → β → m (ForInStep β)) :

m β

We claim this unsafe implementation is correct because an array cannot have more than usizeSz elements in our runtime.

This kind of low level trick can be removed with a little bit of compiler support. For example, if the compiler simplifies as.size < usizeSz to true.

Equations

as.forIn'Unsafe b f = Array.forIn'Unsafe.loop as f as.usize 0 b

@[specialize #[]]

unsafe def Array.forIn'Unsafe.loop {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : (a : α) → a ∈ as → β → m (ForInStep β)) (sz i : USize) (b : β) :

m β

Equations

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

@[implemented_by Array.forIn'Unsafe]

def Array.forIn' {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (b : β) (f : (a : α) → a ∈ as → β → m (ForInStep β)) :

m β

Reference implementation for forIn'

Equations

as.forIn' b f = Array.forIn'.loop as f as.size ⋯ b

def Array.forIn'.loop {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : (a : α) → a ∈ as → β → m (ForInStep β)) (i : Nat) (h : i ≤ as.size) (b : β) :

m β

Equations

One or more equations did not get rendered due to their size.
Array.forIn'.loop as f 0 x_2 b = pure b

instance Array.instForIn'InferInstanceMembership {α : Type u} {m : Type u_1 → Type u_2} :

ForIn' m (Array α) α inferInstance

Equations

Array.instForIn'InferInstanceMembership = { forIn' := fun {β : Type ?u.21} [Monad m] => Array.forIn' }

@[simp]

theorem Array.forIn'_eq_forIn' {α : Type u} {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] :

Array.forIn' = forIn'

@[inline]

unsafe def Array.foldlMUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : β → α → m β) (init : β) (as : Array α) (start : Nat := 0) (stop : Nat := as.size) :

m β

See comment at forIn'Unsafe

Equations

Array.foldlMUnsafe f init as start stop = if start < stop then if stop ≤ as.size then Array.foldlMUnsafe.fold f as (USize.ofNat start) (USize.ofNat stop) init else pure init else pure init

@[specialize #[]]

unsafe def Array.foldlMUnsafe.fold {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : β → α → m β) (as : Array α) (i stop : USize) (b : β) :

m β

Equations

Array.foldlMUnsafe.fold f as i stop b = if (i == stop) = true then pure b else do let __do_lift ← f b (as.uget i ⋯) Array.foldlMUnsafe.fold f as (i + 1) stop __do_lift

@[implemented_by Array.foldlMUnsafe]

def Array.foldlM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : β → α → m β) (init : β) (as : Array α) (start : Nat := 0) (stop : Nat := as.size) :

m β

Reference implementation for foldlM

Equations

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

def Array.foldlM.loop {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : β → α → m β) (as : Array α) (stop : Nat) (h : stop ≤ as.size) (i j : Nat) (b : β) :

m β

Equations

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

@[inline]

unsafe def Array.foldrMUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → β → m β) (init : β) (as : Array α) (start : Nat := as.size) (stop : Nat := 0) :

m β

See comment at forIn'Unsafe

Equations

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

@[specialize #[]]

unsafe def Array.foldrMUnsafe.fold {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → β → m β) (as : Array α) (i stop : USize) (b : β) :

m β

Equations

Array.foldrMUnsafe.fold f as i stop b = if (i == stop) = true then pure b else do let __do_lift ← f (as.uget (i - 1) ⋯) b Array.foldrMUnsafe.fold f as (i - 1) stop __do_lift

@[implemented_by Array.foldrMUnsafe]

def Array.foldrM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → β → m β) (init : β) (as : Array α) (start : Nat := as.size) (stop : Nat := 0) :

m β

Reference implementation for foldrM

Equations

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

def Array.foldrM.fold {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → β → m β) (as : Array α) (stop : Nat := 0) (i : Nat) (h : i ≤ as.size) (b : β) :

m β

Equations

One or more equations did not get rendered due to their size.
Array.foldrM.fold f as stop 0 x_2 b = if (0 == stop) = true then pure b else pure b

@[inline]

unsafe def Array.mapMUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m β) (as : Array α) :

m (Array β)

See comment at forIn'Unsafe

Equations

Array.mapMUnsafe f as = unsafeCast (Array.mapMUnsafe.map f as.usize 0 (unsafeCast as))

@[specialize #[]]

unsafe def Array.mapMUnsafe.map {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m β) (sz i : USize) (bs : Array NonScalar) :

m (Array PNonScalar)

Equations

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

@[implemented_by Array.mapMUnsafe]

def Array.mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m β) (as : Array α) :

m (Array β)

Reference implementation for mapM

Equations

Array.mapM f as = Array.mapM.map f as 0 (Array.mkEmpty as.size)

def Array.mapM.map {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m β) (as : Array α) (i : Nat) (bs : Array β) :

m (Array β)

Equations

Array.mapM.map f as i bs = if hlt : i < as.size then do let __do_lift ← f as[i] Array.mapM.map f as (i + 1) (bs.push __do_lift) else pure bs

@[reducible, inline, deprecated Array.mapM (since := "2024-11-11")]

abbrev Array.sequenceMap {α : Type u_1} {β : Type u_2} {m : Type u_2 → Type u_3} [Monad m] (f : α → m β) (as : Array α) :

m (Array β)

Equations

@Array.sequenceMap = @Array.mapM

@[inline]

def Array.mapFinIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : (i : Nat) → α → i < as.size → m β) :

m (Array β)

Variant of mapIdxM which receives the index i along with the bound i < as.size.

Equations

as.mapFinIdxM f = Array.mapFinIdxM.map as f as.size 0 ⋯ (Array.mkEmpty as.size)

@[specialize #[]]

def Array.mapFinIdxM.map {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : (i : Nat) → α → i < as.size → m β) (i j : Nat) (inv : i + j = as.size) (bs : Array β) :

m (Array β)

Equations

Array.mapFinIdxM.map as f 0 j x bs = pure bs
Array.mapFinIdxM.map as f i_2.succ j inv_2 bs = do let __do_lift ← f j as[j] ⋯ Array.mapFinIdxM.map as f i_2 (j + 1) ⋯ (bs.push __do_lift)

@[inline]

def Array.mapIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : Nat → α → m β) (as : Array α) :

m (Array β)

Equations

Array.mapIdxM f as = as.mapFinIdxM fun (i : Nat) (a : α) (x : i < as.size) => f i a

@[inline]

def Array.firstM {β : Type v} {α : Type u} {m : Type v → Type w} [Alternative m] (f : α → m β) (as : Array α) :

m β

Equations

Array.firstM f as = Array.firstM.go f as 0

@[irreducible]

def Array.firstM.go {β : Type v} {α : Type u} {m : Type v → Type w} [Alternative m] (f : α → m β) (as : Array α) (i : Nat) :

m β

Equations

Array.firstM.go f as i = if hlt : i < as.size then f as[i] <|> Array.firstM.go f as (i + 1) else failure

@[inline]

def Array.findSomeM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m (Option β)) (as : Array α) :

m (Option β)

Equations

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

@[inline]

def Array.findM? {α : Type} {m : Type → Type} [Monad m] (p : α → m Bool) (as : Array α) :

m (Option α)

Note that the universe level is contrained to Type here, to avoid having to have the predicate live in p : α → m (ULift Bool).

Equations

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

@[inline]

def Array.findIdxM? {α : Type u} {m : Type → Type u_1} [Monad m] (p : α → m Bool) (as : Array α) :

m (Option Nat)

Equations

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

@[inline]

unsafe def Array.anyMUnsafe {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Array α) (start : Nat := 0) (stop : Nat := as.size) :

m Bool

Equations

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

@[specialize #[]]

unsafe def Array.anyMUnsafe.any {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Array α) (i stop : USize) :

m Bool

Equations

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

@[implemented_by Array.anyMUnsafe]

def Array.anyM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Array α) (start : Nat := 0) (stop : Nat := as.size) :

m Bool

Equations

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

def Array.anyM.loop {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Array α) (stop : Nat) (h : stop ≤ as.size) (j : Nat) :

m Bool

Equations

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

@[inline]

def Array.allM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Array α) (start : Nat := 0) (stop : Nat := as.size) :

m Bool

Equations

Array.allM p as start stop = do let __do_lift ← Array.anyM (fun (v : α) => do let __do_lift ← p v pure !__do_lift) as start stop pure !__do_lift

@[inline]

def Array.findSomeRevM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m (Option β)) (as : Array α) :

m (Option β)

Equations

Array.findSomeRevM? f as = Array.findSomeRevM?.find f as as.size ⋯

@[specialize #[]]

def Array.findSomeRevM?.find {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m (Option β)) (as : Array α) (i : Nat) :

i ≤ as.size → m (Option β)

Equations

Array.findSomeRevM?.find f as 0 x_2 = pure none
Array.findSomeRevM?.find f as i.succ h = do let r ← f as[i] match r with | some val => pure r | none => let_fun this := ⋯; Array.findSomeRevM?.find f as i this

@[inline]

def Array.findRevM? {α : Type} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Array α) :

m (Option α)

Equations

Array.findRevM? p as = Array.findSomeRevM? (fun (a : α) => do let __do_lift ← p a pure (if __do_lift = true then some a else none)) as

@[inline]

def Array.forM {α : Type u} {m : Type v → Type w} [Monad m] (f : α → m PUnit) (as : Array α) (start : Nat := 0) (stop : Nat := as.size) :

m PUnit

Equations

Array.forM f as start stop = Array.foldlM (fun (x : PUnit) => f) PUnit.unit as start stop

instance Array.instForM {α : Type u} {m : Type u_1 → Type u_2} :

ForM m (Array α) α

Equations

Array.instForM = { forM := fun [Monad m] (xs : Array α) (f : α → m PUnit) => Array.forM f xs }

@[simp]

theorem Array.forM_eq_forM {α : Type u} {m : Type u_1 → Type u_2} {as : Array α} [Monad m] (f : α → m PUnit) :

Array.forM f as = forM as f

@[inline]

def Array.forRevM {α : Type u} {m : Type v → Type w} [Monad m] (f : α → m PUnit) (as : Array α) (start : Nat := as.size) (stop : Nat := 0) :

m PUnit

Equations

Array.forRevM f as start stop = Array.foldrM (fun (a : α) (x : PUnit) => f a) PUnit.unit as start stop

@[inline]

def Array.foldl {α : Type u} {β : Type v} (f : β → α → β) (init : β) (as : Array α) (start : Nat := 0) (stop : Nat := as.size) :

Equations

Array.foldl f init as start stop = (Array.foldlM f init as start stop).run

@[inline]

def Array.foldr {α : Type u} {β : Type v} (f : α → β → β) (init : β) (as : Array α) (start : Nat := as.size) (stop : Nat := 0) :

Equations

Array.foldr f init as start stop = (Array.foldrM f init as start stop).run

@[inline]

def Array.sum {α : Type u_1} [Add α] [Zero α] :

Array α → α

Sum of an array.

Array.sum #[a, b, c] = a + (b + (c + 0))

Equations

as.sum = Array.foldr (fun (x1 x2 : α) => x1 + x2) 0 as

@[inline]

def Array.countP {α : Type u} (p : α → Bool) (as : Array α) :

Nat

Equations

Array.countP p as = Array.foldr (fun (a : α) (acc : Nat) => bif p a then acc + 1 else acc) 0 as

@[inline]

def Array.count {α : Type u} [BEq α] (a : α) (as : Array α) :

Nat

Equations

Array.count a as = Array.countP (fun (x : α) => x == a) as

@[inline]

def Array.map {α : Type u} {β : Type v} (f : α → β) (as : Array α) :

Array β

Equations

Array.map f as = (Array.mapM f as).run

instance Array.instFunctor :

Functor Array

Equations

Array.instFunctor = { map := fun {α β : Type ?u.10} => Array.map, mapConst := fun {α β : Type ?u.10} => Array.map ∘ Function.const β }

@[inline]

def Array.mapFinIdx {α : Type u} {β : Type v} (as : Array α) (f : (i : Nat) → α → i < as.size → β) :

Array β

Variant of mapIdx which receives the index as a Fin as.size.

Equations

as.mapFinIdx f = (as.mapFinIdxM f).run

@[inline]

def Array.mapIdx {α : Type u} {β : Type v} (f : Nat → α → β) (as : Array α) :

Array β

Equations

Array.mapIdx f as = (Array.mapIdxM f as).run

def Array.zipIdx {α : Type u} (xs : Array α) (start : Nat := 0) :

Array (α × Nat)

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

Equations

xs.zipIdx start = Array.mapIdx (fun (i : Nat) (a : α) => (a, start + i)) xs

@[reducible, inline, deprecated Array.zipIdx (since := "2025-01-21")]

abbrev Array.zipWithIndex {α : Type u_1} (xs : Array α) (start : Nat := 0) :

Array (α × Nat)

Equations

@Array.zipWithIndex = @Array.zipIdx

@[inline]

def Array.find? {α : Type u} (p : α → Bool) (as : Array α) :

Option α

Equations

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

@[inline]

def Array.findSome? {α : Type u} {β : Type v} (f : α → Option β) (as : Array α) :

Option β

Equations

Array.findSome? f as = (Array.findSomeM? f as).run

@[inline]

def Array.findSome! {α : Type u} {β : Type v} [Inhabited β] (f : α → Option β) (xs : Array α) :

Equations

Array.findSome! f xs = match Array.findSome? f xs with | some b => b | none => panicWithPosWithDecl "Init.Data.Array.Basic" "Array.findSome!" 708 14 "failed to find element"

@[inline]

def Array.findSomeRev? {α : Type u} {β : Type v} (f : α → Option β) (as : Array α) :

Option β

Equations

Array.findSomeRev? f as = (Array.findSomeRevM? f as).run

@[inline]

def Array.findRev? {α : Type} (p : α → Bool) (as : Array α) :

Option α

Equations

Array.findRev? p as = (Array.findRevM? p as).run

@[inline]

def Array.findIdx? {α : Type u} (p : α → Bool) (as : Array α) :

Equations

Array.findIdx? p as = Array.findIdx?.loop p as 0

def Array.findIdx?.loop {α : Type u} (p : α → Bool) (as : Array α) (j : Nat) :

Equations

Array.findIdx?.loop p as j = if h : j < as.size then if p as[j] = true then some j else Array.findIdx?.loop p as (j + 1) else none

@[inline]

def Array.findFinIdx? {α : Type u} (p : α → Bool) (as : Array α) :

Option (Fin as.size)

Equations

Array.findFinIdx? p as = Array.findFinIdx?.loop p as 0

def Array.findFinIdx?.loop {α : Type u} (p : α → Bool) (as : Array α) (j : Nat) :

Option (Fin as.size)

Equations

Array.findFinIdx?.loop p as j = if h : j < as.size then if p as[j] = true then some ⟨j, h⟩ else Array.findFinIdx?.loop p as (j + 1) else none

@[irreducible]

theorem Array.findIdx?_loop_eq_map_findFinIdx?_loop_val {α : Type u} {xs : Array α} {p : α → Bool} {j : Nat} :

findIdx?.loop p xs j = Option.map (fun (x : Fin xs.size) => ↑x) (findFinIdx?.loop p xs j)

theorem Array.findIdx?_eq_map_findFinIdx?_val {α : Type u} {xs : Array α} {p : α → Bool} :

findIdx? p xs = Option.map (fun (x : Fin xs.size) => ↑x) (findFinIdx? p xs)

@[inline]

def Array.findIdx {α : Type u} (p : α → Bool) (as : Array α) :

Nat

Equations

Array.findIdx p as = (Array.findIdx? p as).getD as.size

def Array.idxOfAux {α : Type u} [BEq α] (xs : Array α) (v : α) (i : Nat) :

Option (Fin xs.size)

Equations

xs.idxOfAux v i = if h : i < xs.size then if (xs[i] == v) = true then some ⟨i, h⟩ else xs.idxOfAux v (i + 1) else none

@[reducible, inline, deprecated Array.idxOfAux (since := "2025-01-29")]

abbrev Array.indexOfAux {α : Type u_1} [BEq α] (xs : Array α) (v : α) (i : Nat) :

Option (Fin xs.size)

Equations

@Array.indexOfAux = @Array.idxOfAux

def Array.finIdxOf? {α : Type u} [BEq α] (xs : Array α) (v : α) :

Option (Fin xs.size)

Equations

xs.finIdxOf? v = xs.idxOfAux v 0

@[reducible, inline, deprecated "`Array.indexOf?` has been deprecated, use `idxOf?` or `finIdxOf?` instead." (since := "2025-01-29")]

abbrev Array.indexOf? {α : Type u_1} [BEq α] (xs : Array α) (v : α) :

Option (Fin xs.size)

Equations

@Array.indexOf? = @Array.finIdxOf?

def Array.idxOf {α : Type u} [BEq α] (a : α) :

Array α → Nat

Returns the index of the first element equal to a, or the length of the array otherwise.

Equations

Array.idxOf a = Array.findIdx fun (x : α) => x == a

def Array.idxOf? {α : Type u} [BEq α] (xs : Array α) (v : α) :

Equations

xs.idxOf? v = Option.map (fun (x : Fin xs.size) => ↑x) (xs.finIdxOf? v)

@[deprecated Array.idxOf? (since := "2024-11-20")]

def Array.getIdx? {α : Type u} [BEq α] (xs : Array α) (v : α) :

Equations

xs.getIdx? v = Array.findIdx? (fun (a : α) => a == v) xs

@[inline]

def Array.any {α : Type u} (as : Array α) (p : α → Bool) (start : Nat := 0) (stop : Nat := as.size) :

Equations

as.any p start stop = (Array.anyM p as start stop).run

@[inline]

def Array.all {α : Type u} (as : Array α) (p : α → Bool) (start : Nat := 0) (stop : Nat := as.size) :

Equations

as.all p start stop = (Array.allM p as start stop).run

def Array.contains {α : Type u} [BEq α] (as : Array α) (a : α) :

as.contains a is true if there is some element b in as such that a == b.

Equations

as.contains a = as.any fun (x : α) => a == x

def Array.elem {α : Type u} [BEq α] (a : α) (as : Array α) :

Variant of Array.contains with arguments reversed.

For verification purposes, we simplify this to contains.

Equations

Array.elem a as = as.contains a

@[export lean_array_to_list_impl]

def Array.toListImpl {α : Type u} (as : Array α) :

List α

Convert a Array α into an List α. This is O(n) in the size of the array.

Equations

as.toListImpl = Array.foldr List.cons [] as

@[inline]

def Array.toListAppend {α : Type u} (as : Array α) (l : List α) :

List α

Prepends an Array α onto the front of a list. Equivalent to as.toList ++ l.

Equations

as.toListAppend l = Array.foldr List.cons l as

def Array.append {α : Type u} (as bs : Array α) :

Array α

Equations

as.append bs = Array.foldl (fun (xs : Array α) (v : α) => xs.push v) as bs

instance Array.instAppend {α : Type u} :

Append (Array α)

Equations

Array.instAppend = { append := Array.append }

def Array.appendList {α : Type u} (as : Array α) (bs : List α) :

Array α

Equations

as.appendList bs = List.foldl (fun (xs : Array α) (v : α) => xs.push v) as bs

instance Array.instHAppendList {α : Type u} :

HAppend (Array α) (List α) (Array α)

Equations

Array.instHAppendList = { hAppend := Array.appendList }

@[inline]

def Array.flatMapM {α : Type u} {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] (f : α → m (Array β)) (as : Array α) :

m (Array β)

Equations

Array.flatMapM f as = Array.foldlM (fun (bs : Array β) (a : α) => do let __do_lift ← f a pure (bs ++ __do_lift)) #[] as

@[reducible, inline, deprecated Array.flatMapM (since := "2024-10-16")]

abbrev Array.concatMapM {α : Type u_1} {m : Type u_2 → Type u_3} {β : Type u_2} [Monad m] (f : α → m (Array β)) (as : Array α) :

m (Array β)

Equations

@Array.concatMapM = @Array.flatMapM

@[inline]

def Array.flatMap {α : Type u} {β : Type u_1} (f : α → Array β) (as : Array α) :

Array β

Equations

Array.flatMap f as = Array.foldl (fun (bs : Array β) (a : α) => bs ++ f a) #[] as

@[reducible, inline, deprecated Array.flatMap (since := "2024-10-16")]

abbrev Array.concatMap {α : Type u_1} {β : Type u_2} (f : α → Array β) (as : Array α) :

Array β

Equations

@Array.concatMap = @Array.flatMap

@[inline]

def Array.flatten {α : Type u} (xss : Array (Array α)) :

Array α

Joins array of array into a single array.

flatten #[#[a₁, a₂, ⋯], #[b₁, b₂, ⋯], ⋯] = #[a₁, a₂, ⋯, b₁, b₂, ⋯]

Equations

xss.flatten = Array.foldl (fun (acc xs : Array α) => acc ++ xs) #[] xss

def Array.reverse {α : Type u} (as : Array α) :

Array α

Equations

as.reverse = if h : as.size ≤ 1 then as else Array.reverse.loop as 0 ⟨as.size - 1, ⋯⟩

theorem Array.reverse.termination {i j : Nat} (h : i < j) :

j - 1 - (i + 1) < j - i

@[irreducible]

def Array.reverse.loop {α : Type u} (as : Array α) (i : Nat) (j : Fin as.size) :

Array α

Equations

Array.reverse.loop as i j = if h : i < ↑j then let_fun this := ⋯; let as_1 := as.swap i ↑j ⋯ ⋯; let_fun this := ⋯; Array.reverse.loop as_1 (i + 1) ⟨↑j - 1, this⟩ else as

@[inline]

def Array.filter {α : Type u} (p : α → Bool) (as : Array α) (start : Nat := 0) (stop : Nat := as.size) :

Array α

Equations

Array.filter p as start stop = Array.foldl (fun (acc : Array α) (a : α) => if p a = true then acc.push a else acc) #[] as start stop

@[inline]

def Array.filterM {m : Type → Type u_1} {α : Type} [Monad m] (p : α → m Bool) (as : Array α) (start : Nat := 0) (stop : Nat := as.size) :

m (Array α)

Equations

Array.filterM p as start stop = Array.foldlM (fun (acc : Array α) (a : α) => do let __do_lift ← p a if __do_lift = true then pure (acc.push a) else pure acc) #[] as start stop

@[inline]

def Array.filterRevM {m : Type → Type u_1} {α : Type} [Monad m] (p : α → m Bool) (as : Array α) (start : Nat := as.size) (stop : Nat := 0) :

m (Array α)

Equations

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

@[specialize #[]]

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

m (Array β)

Equations

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

@[inline]

def Array.filterMap {α : Type u} {β : Type u_1} (f : α → Option β) (as : Array α) (start : Nat := 0) (stop : Nat := as.size) :

Array β

Equations

Array.filterMap f as start stop = (Array.filterMapM f as start stop).run

@[specialize #[]]

def Array.getMax? {α : Type u} (as : Array α) (lt : α → α → Bool) :

Option α

Equations

as.getMax? lt = if h : 0 < as.size then let a0 := as[0]; some (Array.foldl (fun (best a : α) => if lt best a = true then a else best) a0 as 1) else none

@[inline]

def Array.partition {α : Type u} (p : α → Bool) (as : Array α) :

Array α × Array α

Equations

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

def Array.popWhile {α : Type u} (p : α → Bool) (as : Array α) :

Array α

Equations

Array.popWhile p as = if h : as.size > 0 then if p as[as.size - 1] = true then Array.popWhile p as.pop else as else as

@[simp]

theorem Array.popWhile_empty {α : Type u} (p : α → Bool) :

popWhile p #[] = #[]

def Array.takeWhile {α : Type u} (p : α → Bool) (as : Array α) :

Array α

Equations

Array.takeWhile p as = Array.takeWhile.go p as 0 #[]

def Array.takeWhile.go {α : Type u} (p : α → Bool) (as : Array α) (i : Nat) (acc : Array α) :

Array α

Equations

Array.takeWhile.go p as i acc = if h : i < as.size then let a := as[i]; if p a = true then Array.takeWhile.go p as (i + 1) (acc.push a) else acc else acc

def Array.eraseIdx {α : Type u} (xs : Array α) (i : Nat) (h : i < xs.size := by get_elem_tactic) :

Array α

Remove the element at a given index from an array without a runtime bounds checks, using a Nat index and a tactic-provided bound.

This function takes worst case O(n) time because it has to backshift all elements at positions greater than i.

Equations

xs.eraseIdx i h = if h' : i + 1 < xs.size then let xs' := xs.swap (i + 1) i h' h; xs'.eraseIdx (i + 1) ⋯ else xs.pop

@[simp]

theorem Array.size_eraseIdx {α : Type u} (xs : Array α) (i : Nat) (h : i < xs.size) :

(xs.eraseIdx i h).size = xs.size - 1

def Array.eraseIdxIfInBounds {α : Type u} (xs : Array α) (i : Nat) :

Array α

Remove the element at a given index from an array, or do nothing if the index is out of bounds.

This function takes worst case O(n) time because it has to backshift all elements at positions greater than i.

Equations

xs.eraseIdxIfInBounds i = if h : i < xs.size then xs.eraseIdx i h else xs

def Array.eraseIdx! {α : Type u} (xs : Array α) (i : Nat) :

Array α

Remove the element at a given index from an array, or panic if the index is out of bounds.

This function takes worst case O(n) time because it has to backshift all elements at positions greater than i.

Equations

xs.eraseIdx! i = if h : i < xs.size then xs.eraseIdx i h else panicWithPosWithDecl "Init.Data.Array.Basic" "Array.eraseIdx!" 978 47 "invalid index"

def Array.erase {α : Type u} [BEq α] (as : Array α) (a : α) :

Array α

Remove a specified element from an array, or do nothing if it is not present.

This function takes worst case O(n) time because it has to backshift all later elements.

Equations

as.erase a = match as.finIdxOf? a with | none => as | some i => as.eraseIdx ↑i ⋯

def Array.eraseP {α : Type u} (as : Array α) (p : α → Bool) :

Array α

Erase the first element that satisfies the predicate p.

This function takes worst case O(n) time because it has to backshift all later elements.

Equations

as.eraseP p = match Array.findFinIdx? p as with | none => as | some i => as.eraseIdx ↑i ⋯

@[inline]

def Array.insertIdx {α : Type u} (as : Array α) (i : Nat) (a : α) :

autoParam (i ≤ as.size) _auto✝ → Array α

Insert element a at position i.

This function takes worst case O(n) time because it has to swap the inserted element into place.

Equations

as.insertIdx i a x✝ = Array.insertIdx.loop i (as.push a) ⟨as.size, ⋯⟩

def Array.insertIdx.loop {α : Type u} (i : Nat) (as : Array α) (j : Fin as.size) :

Array α

Equations

Array.insertIdx.loop i as j = if i < ↑j then let j' := ⟨↑j - 1, ⋯⟩; let as_1 := as.swap ↑j' ↑j ⋯ ⋯; Array.insertIdx.loop i as_1 ⟨↑j', ⋯⟩ else as

@[reducible, inline, deprecated Array.insertIdx (since := "2024-11-20")]

abbrev Array.insertAt {α : Type u_1} (as : Array α) (i : Nat) (a : α) :

autoParam (i ≤ as.size) _auto✝ → Array α

Equations

@Array.insertAt = @Array.insertIdx

def Array.insertIdx! {α : Type u} (as : Array α) (i : Nat) (a : α) :

Array α

Insert element a at position i. Panics if i is not i ≤ as.size.

Equations

as.insertIdx! i a = if h : i ≤ as.size then as.insertIdx i a h else panicWithPosWithDecl "Init.Data.Array.Basic" "Array.insertIdx!" 1023 7 "invalid index"

@[reducible, inline, deprecated Array.insertIdx! (since := "2024-11-20")]

abbrev Array.insertAt! {α : Type u_1} (as : Array α) (i : Nat) (a : α) :

Array α

Equations

@Array.insertAt! = @Array.insertIdx!

def Array.insertIdxIfInBounds {α : Type u} (as : Array α) (i : Nat) (a : α) :

Array α

Insert element a at position i, or do nothing if as.size < i.

Equations

as.insertIdxIfInBounds i a = if h : i ≤ as.size then as.insertIdx i a h else as

def Array.isPrefixOfAux {α : Type u} [BEq α] (as bs : Array α) (hle : as.size ≤ bs.size) (i : Nat) :

Equations

as.isPrefixOfAux bs hle i = if h : i < as.size then let a := as[i]; let_fun this := ⋯; let b := bs[i]; if (a == b) = true then as.isPrefixOfAux bs hle (i + 1) else false else true

def Array.isPrefixOf {α : Type u} [BEq α] (as bs : Array α) :

Return true iff as is a prefix of bs. That is, bs = as ++ t for some t : List α.

Equations

as.isPrefixOf bs = if h : as.size ≤ bs.size then as.isPrefixOfAux bs h 0 else false

@[specialize #[]]

def Array.zipWithAux {α : Type u} {β : Type u_1} {γ : Type u_2} (as : Array α) (bs : Array β) (f : α → β → γ) (i : Nat) (cs : Array γ) :

Array γ

Equations

as.zipWithAux bs f i cs = if h : i < as.size then let a := as[i]; if h : i < bs.size then let b := bs[i]; as.zipWithAux bs f (i + 1) (cs.push (f a b)) else cs else cs

@[inline]

def Array.zipWith {α : Type u} {β : Type u_1} {γ : Type u_2} (f : α → β → γ) (as : Array α) (bs : Array β) :

Array γ

Equations

Array.zipWith f as bs = as.zipWithAux bs f 0 #[]

def Array.zip {α : Type u} {β : Type u_1} (as : Array α) (bs : Array β) :

Array (α × β)

Equations

as.zip bs = Array.zipWith Prod.mk as bs

def Array.zipWithAll {α : Type u} {β : Type u_1} {γ : Type u_2} (f : Option α → Option β → γ) (as : Array α) (bs : Array β) :

Array γ

Equations

Array.zipWithAll f as bs = Array.zipWithAll.go f as bs 0 #[]

@[irreducible]

def Array.zipWithAll.go {α : Type u} {β : Type u_1} {γ : Type u_2} (f : Option α → Option β → γ) (as : Array α) (bs : Array β) (i : Nat) (cs : Array γ) :

Array γ

Equations

Array.zipWithAll.go f as bs i cs = if i < max as.size bs.size then let a := as[i]?; let b := bs[i]?; Array.zipWithAll.go f as bs (i + 1) (cs.push (f a b)) else cs