14.16. Arrays🔗

The Array type represents sequences of elements, addressable by their position in the sequence. Arrays are specially supported by Lean:

They have a logical model that specifies their behavior in terms of lists of elements, which specifies the meaning of each operation on arrays.
They have an optimized run-time representation in compiled code as dynamic arrays, and the Lean runtime specially optimizes array operations.
There is array literal syntax for writing arrays.

Arrays can be vastly more efficient than lists or other sequences in compiled code. In part, this is because they offer good locality: because all the elements of the sequence are next to each other in memory, the processor's caches can be used efficiently. Even more importantly, if there is only a single reference to an array, operations that might otherwise copy or allocate a data structure can be implemented via mutation. Lean code that uses an array in such a way that there's only ever one unique reference (that is, uses it linearly) avoids the performance overhead of persistent data structures while still being as convenient to write, read, and prove things about as ordinary pure functional programs.

14.16.1. Logical Model

structure

Array.{u} (α : Type u) : Type u

Array α is the type of dynamic arrays with elements from α. This type has special support in the runtime.

An array has a size and a capacity; the size is Array.size but the capacity is not observable from Lean code. Arrays perform best when unshared; as long as they are used "linearly" all updates will be performed destructively on the array, so it has comparable performance to mutable arrays in imperative programming languages.

From the point of view of proofs Array α is just a wrapper around List α.

Constructor

Array.mk.{u}

Converts a List α into an Array α.

You can also use the synonym List.toArray when dot notation is convenient.

At runtime, this constructor is implemented by List.toArrayImpl and is O(n) in the length of the list.

Fields

toList : List α

Converts a Array α into an List α.

At runtime, this projection is implemented by Array.toListImpl and is O(n) in the length of the array.

The logical model of arrays is a structure that contains a single field, which is a list of elements. This is convenient when specifying and proving properties of array-processing functions at a low level.

14.16.2. Run-Time Representation🔗

Lean's arrays are dynamic arrays, which are blocks of continuous memory with a defined capacity, not all of which is typically in use. As long as the number of elements in the array is less than the capacity, new items can be added to the end without reallocating or moving the data. Adding items to an array that has no extra space results in a reallocation that doubles the capacity. The amortized overhead scales linearly with the size of the array. The values in the array are represented as described in the section on the foreign function interface.

After the object header, an array contains:

size: The number of objects currently stored in the array
capacity: The number of objects that fit in the memory allocated for the array
data: The values in the array

Many array functions in the Lean runtime check whether they have exclusive access to their argument by consulting the reference count in the object header. If they do, and the array's capacity is sufficient, then the existing array can be mutated rather than allocating fresh memory. Otherwise, a new array must be allocated.

14.16.2.1. Performance Notes🔗

Despite the fact that they appear to be an ordinary constructor and projection, Array.mk and Array.data take time linear in the size of the array in compiled code. This is because they must implement the conversions between linked lists and packed arrays, which must necessarily visit each element.

Mutable arrays can be used to write very efficient code. However, they are a poor persistent data structure. Updating a shared array rules out mutation, and requires time linear in the size of the array. When using arrays in performance-critical code, it's important to ensure that they are used linearly.

14.16.3. Syntax🔗

Array literals allow arrays to be written directly in code. They may be used in expression or pattern contexts.

syntax

Array literals begin with #[ and contain a comma-separated sequence of terms, terminating with ].

term ::= ...
    | Syntax for `Array α`. 

Conventions for notations in identifiers:

 * The recommended spelling of `#[]` in identifiers is `empty`.

 * The recommended spelling of `#[x]` in identifiers is `singleton`.#[term,*]

Array Literals

Array literals may be used as expressions or as patterns.

def oneTwoThree : Array Nat := #[1, 2, 3]

some 2#eval
  match oneTwoThree with
  | #[x, y, z] => some ((x + z) / y)
  | _ => none

Additionally, sub-arrays may be extracted using the following syntax:

syntax

A start index followed by a colon constructs a sub-array that contains the values from the start index onwards (inclusive):

term ::= ...
    | term[term :]

Providing start and end indices constructs a sub-array that contains the values from the start index (inclusive) to the end index (exclusive):

term ::= ...
    | term[term : term]

Sub-array Syntax

The array ten contains the first ten natural numbers.

def ten : Array Nat :=
  .range 10

A sub-array that represents the second half of ten can be constructed using the sub-array syntax:

#[5, 6, 7, 8, 9].toSubarray#eval ten[5:]

#[5, 6, 7, 8, 9].toSubarray

Similarly, sub-array that contains two through five can be constructed by providing a stopping point:

#[2, 3, 4, 5].toSubarray#eval ten[2:6]

#[2, 3, 4, 5].toSubarray

Because sub-arrays merely store the start and end indices of interest in the underlying array, the array itself can be recovered:

true#eval ten[2:6].array == ten

true

14.16.4. API Reference🔗

14.16.4.1. Constructing Arrays

def

Array.empty.{u} {α : Type u} : Array α

Construct a new empty array.

def

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

def

Array.range (n : Nat) : Array Nat

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

def

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

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

def

Array.finRange (n : Nat) : Array (Fin n)

finRange n is the array of all elements of Fin n in order.

def

Array.ofFn.{u} {α : 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)]

def

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

def

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

def

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

14.16.4.2. Size

def

Array.size.{u} {α : Type u} (a : Array α) : Nat

Get the size of an array. This is a cached value, so it is O(1) to access.

def

Array.usize.{u} {α : 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.

def

Array.isEmpty.{u} {α : Type u} (a : Array α) :
  Bool

14.16.4.3. Lookups

def

Array.extract.{u_1} {α : Type u_1}
  (as : Array α) (start : Nat := 0)
  (stop : Nat := as.size) : Array α

Returns the slice of as from indices start to stop (exclusive). If start is greater or equal to stop, the result is empty. If stop is greater than the length of as, the length is used instead.

def

Array.getD.{u_1} {α : Type u_1} (a : Array α)
  (i : Nat) (v₀ : α) : α

Access an element from an array, or return v₀ if the index is out of bounds.

def

Array.uget.{u} {α : 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.

def

Array.back?.{u} {α : Type u} (a : 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.

def

Array.back!.{u} {α : Type u} [Inhabited α]
  (a : 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.

def

Array.back.{u} {α : Type u} (a : Array α)
  (h : 0 < a.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.

def

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

14.16.4.4. Queries

def

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

def

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

def

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

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

def

Array.idxOf?.{u} {α : Type u} [BEq α]
  (a : Array α) (v : α) : Option Nat

def

Array.finIdxOf?.{u} {α : Type u} [BEq α]
  (a : Array α) (v : α) : Option (Fin a.size)

14.16.4.5. Conversions

def

Array.toList.{u} {α : Type u} (self : Array α) :
  List α

Converts a Array α into an List α.

At runtime, this projection is implemented by Array.toListImpl and is O(n) in the length of the array.

def

Array.toListRev.{u_1} {α : Type u_1}
  (arr : Array α) : List α

A more efficient version of arr.toList.reverse.

def

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

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

def

Array.toVector.{u_1} {α : Type u_1}
  (xs : Array α) : Vector α xs.size

Convert xs : Array α to Vector α xs.size.

def

Array.toSubarray.{u} {α : Type u} (as : Array α)
  (start : Nat := 0) (stop : Nat := as.size) :
  Subarray α

def

Array.ofSubarray.{u} {α : Type u}
  (s : Subarray α) : Array α

def

Array.toPArray'.{u} {α : Type u}
  (xs : Array α) : Lean.PersistentArray α

14.16.4.6. Modification

def

Array.push.{u} {α : Type u} (a : Array α)
  (v : α) : Array α

Push an element onto the end of an array. This is amortized O(1) because Array α is internally a dynamic array.

def

Array.pop.{u} {α : Type u} (a : Array α) :
  Array α

def

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

def

Array.erase.{u} {α : 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.

def

Array.eraseP.{u} {α : 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.

def

Array.eraseIdx.{u} {α : Type u} (a : Array α)
  (i : Nat)
  (h : i < a.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.

def

Array.eraseIdx!.{u} {α : Type u} (a : 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.

def

Array.eraseIdxIfInBounds.{u} {α : Type u}
  (a : 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.

def

Array.eraseReps.{u_1} {α : Type u_1} [BEq α]
  (as : Array α) : Array α

O(|l|). Erase repeated adjacent elements. Keeps the first occurrence of each run.

eraseReps #[1, 3, 2, 2, 2, 3, 5] = #[1, 3, 2, 3, 5]

def

Array.swap.{u} {α : Type u} (a : Array α)
  (i j : Nat)
  (hi : i < a.size := by get_elem_tactic)
  (hj : j < a.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.

def

Array.swapIfInBounds.{u} {α : Type u}
  (a : 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.

def

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

def

Array.swapAt!.{u} {α : Type u} (a : Array α)
  (i : Nat) (v : α) : α × Array α

def

Array.set.{u_1} {α : Type u_1} (a : Array α)
  (i : Nat) (v : α)
  (h : i < a.size := by get_elem_tactic) :
  Array α

Set an element in an array, using a proof that the index is in bounds. (This proof can usually be omitted, and will be synthesized automatically.)

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

def

Array.set!.{u_1} {α : Type u_1} (a : Array α)
  (i : Nat) (v : α) : Array α

Set an element in an array, or panic if the index is out of bounds.

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

def

Array.setIfInBounds.{u_1} {α : Type u_1}
  (a : Array α) (i : Nat) (v : α) : Array α

Set an element in an array, or do nothing if the index is out of bounds.

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

def

Array.uset.{u} {α : Type u} (a : Array α)
  (i : USize) (v : α) (h : i.toNat < a.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.

def

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

def

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

def

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

def

Array.insertIdx.{u} {α : 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.

def

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

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

def

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

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

def

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

def

Array.binInsertM.{u, v} {α : Type u}
  {m : Type u → Type v} [Monad m]
  (lt : α → α → Bool) (merge : α → m α)
  (add : Unit → m α) (as : Array α) (k : α) :
  m (Array α)

def

Array.take.{u} {α : Type u} (a : Array α)
  (n : Nat) : Array α

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

def

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

def

Array.drop.{u} {α : Type u} (a : Array α)
  (n : Nat) : Array α

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

def

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

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

def

Array.flatten.{u} {α : Type u}
  (as : Array (Array α)) : Array α

Joins array of array into a single array.

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

def

Array.getEvenElems.{u} {α : Type u}
  (as : Array α) : Array α

14.16.4.7. Sorted Arrays

def

Array.qsort.{u_1} {α : Type u_1} (as : Array α)
  (lt : α → α → Bool := by exact (· < ·))
  (low : Nat := 0) (high : Nat := as.size - 1) :
  Array α

def

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

Sort an array using compare to compare elements.

def

Array.insertionSort.{u_1} {α : Type u_1}
  (a : Array α)
  (lt : α → α → Bool := by exact (· < ·)) :
  Array α

def

Array.binInsert.{u} {α : Type u}
  (lt : α → α → Bool) (as : Array α) (k : α) :
  Array α

def

Array.binSearch {α : Type} (as : Array α)
  (k : α) (lt : α → α → Bool) (lo : Nat := 0)
  (hi : Nat := as.size - 1) : Option α

def

Array.binSearchContains {α : Type}
  (as : Array α) (k : α) (lt : α → α → Bool)
  (lo : Nat := 0) (hi : Nat := as.size - 1) :
  Bool

14.16.4.8. Iteration

def

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

def

Array.foldrM.{u, v, w} {α : 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

def

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

def

Array.foldlM.{u, v, w} {α : 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

def

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

def

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

def

Array.forIn'.{u, v, w} {α : 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'

def

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

def

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

Sum of an array.

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

14.16.4.9. Transformation

def

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

def

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

def

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

def

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

def

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

def

Array.zipIdx.{u} {α : Type u} (arr : Array α)
  (start : Nat := 0) : Array (α × Nat)

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

def

Array.unzip.{u, u_1} {α : Type u} {β : Type u_1}
  (as : Array (α × β)) : Array α × Array β

def

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

def

Array.mapMono.{u_1} {α : Type u_1}
  (as : Array α) (f : α → α) : Array α

def

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

Reference implementation for mapM

def

Array.mapM'.{u_1, u_2, u_3}
  {m : Type u_1 → Type u_2} {α : Type u_3}
  {β : Type u_1} [Monad m] (f : α → m β)
  (as : Array α) : m { bs // bs.size = as.size }

def

Array.mapMonoM.{u_1, u_2}
  {m : Type u_1 → Type u_2} {α : Type u_1}
  [Monad m] (as : Array α) (f : α → m α) :
  m (Array α)

Monomorphic Array.mapM. The internal implementation uses pointer equality, and does not allocate a new array if the result of each f a is a pointer equal value a.

def

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

def

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

def

Array.mapFinIdx.{u, v} {α : 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.

def

Array.mapIndexed.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} (arr : Array α)
  (f : Fin arr.size → α → β) : Array β

def

Array.mapIndexedM.{u_1, u_2, u_3}
  {m : Type u_1 → Type u_2} {α : Type u_3}
  {β : Type u_1} [Monad m] (arr : Array α)
  (f : Fin arr.size → α → m β) : m (Array β)

def

Array.mapFinIdxM.{u, v, w} {α : 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.

def

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

def

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

14.16.4.10. Filtering

def

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

def

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

def

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

def

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

def

Array.filterMapM.{u, u_1, u_2} {α : 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 β)

def

Array.filterPairsM.{u_1} {m : Type → Type u_1}
  [Monad m] {α : Type} (a : Array α)
  (f : α → α → m (Bool × Bool)) : m (Array α)

Given an array a, runs f xᵢ xⱼ for all i < j, removes those entries for which f returns false (and will subsequently skip pairs if one element is removed), and returns the array of remaining elements.

This can be used to remove elements from an array where a “better” element, in some partial order, exists in the array.

def

Array.filterSepElems (a : Array Lean.Syntax)
  (p : Lean.Syntax → Bool) : Array Lean.Syntax

def

Array.filterSepElemsM {m : Type → Type}
  [Monad m] (a : Array Lean.Syntax)
  (p : Lean.Syntax → m Bool) :
  m (Array Lean.Syntax)

14.16.4.11. Partitioning

def

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

def

Array.groupByKey.{u, v} {α : Type u}
  {β : Type v} [BEq α] [Hashable α]
  (key : β → α) (xs : Array β) :
  Std.HashMap α (Array β)

Groups all elements x, y in xs with key x == key y into the same array (xs.groupByKey key).find! (key x). Groups preserve the relative order of elements in xs.

14.16.4.12. Element Predicates

def

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

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

def

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

Variant of Array.contains with arguments reversed.

For verification purposes, we simplify this to contains.

def

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

def

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

def

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

def

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

def

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

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

def

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

def

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

def

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

def

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

def

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

def

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

def

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

def

Array.allDiff.{u} {α : Type u} [BEq α]
  (as : Array α) : Bool

def

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

def

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

def

Array.isEqv.{u} {α : Type u} (a b : Array α)
  (p : α → α → Bool) : Bool

def

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

def

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

14.16.4.13. Comparisons

def

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

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

def

Array.lex.{u_1} {α : Type u_1} [BEq α]
  (as bs : Array α)
  (lt : α → α → Bool := by exact (· < ·)) : Bool

Lexicographic comparator for arrays.

lex as bs lt is true if

bs is larger than as and as is pairwise equivalent via == to the initial segment of bs, or
there is an index i such that lt as[i] bs[i], and for all j < i, as[j] == bs[j].

14.16.4.14. Termination Helpers

def

Array.attach.{u_1} {α : 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}.

def

Array.attachWith.{u_1} {α : 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}.

def

Array.unattach.{u_1} {α : Type u_1}
  {p : α → Prop} (l : Array { x // p x }) :
  Array α

A synonym for l.map (·.val). Mostly this should not be needed by users. It is introduced as in intermediate step by lemmas such as map_subtype, and is ideally subsequently simplified away by unattach_attach.

If not, usually the right approach is simp [Array.unattach, -Array.map_subtype] to unfold.

def

Array.pmap.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} {P : α → Prop}
  (f : (a : α) → P a → β) (l : Array α)
  (H : ∀ (a : α), a ∈ l → P a) : Array β

O(n). Partial map. If f : Π a, P a → β is a partial function defined on a : α satisfying P, then pmap f l h is essentially the same as map f l but is defined only when all members of l satisfy P, using the proof to apply f.

We replace this at runtime with a more efficient version via the csimp lemma pmap_eq_pmapImpl.

14.16.4.15. Proof Automation

def

Array.reduceOption.{u} {α : Type u}
  (as : Array (Option α)) : Array α

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

def

Array.reduceGetElem : Lean.Meta.Simp.DSimproc

Simplification procedure for #[...][n] for n a Nat literal.

def

Array.reduceGetElem? : Lean.Meta.Simp.DSimproc

Simplification procedure for #[...][n]? for n a Nat literal.

def

Array.reduceGetElem! : Lean.Meta.Simp.DSimproc

Simplification procedure for #[...][n]! for n a Nat literal.

14.16.5. Sub-Arrays🔗

structure

Subarray.{u} (α : Type u) : Type u

Constructor

Subarray.mk.{u}

Fields

array : Array α

start : Nat

stop : Nat

start_le_stop : self.start ≤ self.stop

stop_le_array_size : self.stop ≤ self.array.size

def

Subarray.toArray.{u_1} {α : Type u_1}
  (s : Subarray α) : Array α

def

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

The empty subarray.

14.16.5.1. Size

def

Subarray.size.{u_1} {α : Type u_1}
  (s : Subarray α) : Nat

14.16.5.2. Resizing

def

Subarray.drop.{u_1} {α : Type u_1}
  (arr : Subarray α) (i : Nat) : Subarray α

Removes the first i elements of the subarray. If there are i or fewer elements, the resulting subarray is empty.

def

Subarray.take.{u_1} {α : Type u_1}
  (arr : Subarray α) (i : Nat) : Subarray α

Keeps only the first i elements of the subarray. If there are i or fewer elements, the resulting subarray is empty.

def

Subarray.popFront.{u_1} {α : Type u_1}
  (s : Subarray α) : Subarray α

def

Subarray.split.{u_1} {α : Type u_1}
  (s : Subarray α) (i : Fin s.size.succ) :
  Subarray α × Subarray α

Splits a subarray into two parts.

14.16.5.3. Lookups

def

Subarray.get.{u_1} {α : Type u_1}
  (s : Subarray α) (i : Fin s.size) : α

def

Subarray.get!.{u_1} {α : Type u_1} [Inhabited α]
  (s : Subarray α) (i : Nat) : α

def

Subarray.getD.{u_1} {α : Type u_1}
  (s : Subarray α) (i : Nat) (v₀ : α) : α

14.16.5.4. Iteration

def

Subarray.foldl.{u, v} {α : Type u} {β : Type v}
  (f : β → α → β) (init : β) (as : Subarray α) :
  β

def

Subarray.foldlM.{u, v, w} {α : Type u}
  {β : Type v} {m : Type v → Type w} [Monad m]
  (f : β → α → m β) (init : β)
  (as : Subarray α) : m β

def

Subarray.foldr.{u, v} {α : Type u} {β : Type v}
  (f : α → β → β) (init : β) (as : Subarray α) :
  β

def

Subarray.foldrM.{u, v, w} {α : Type u}
  {β : Type v} {m : Type v → Type w} [Monad m]
  (f : α → β → m β) (init : β)
  (as : Subarray α) : m β

def

Subarray.forM.{u, v, w} {α : Type u}
  {m : Type v → Type w} [Monad m]
  (f : α → m PUnit) (as : Subarray α) : m PUnit

def

Subarray.forRevM.{u, v, w} {α : Type u}
  {m : Type v → Type w} [Monad m]
  (f : α → m PUnit) (as : Subarray α) : m PUnit

opaque

Subarray.forIn.{u, v, w} {α : Type u}
  {β : Type v} {m : Type v → Type w} [Monad m]
  (s : Subarray α) (b : β)
  (f : α → β → m (ForInStep β)) : m β

14.16.5.5. Element Predicates

def

Subarray.findRev? {α : Type} (as : Subarray α)
  (p : α → Bool) : Option α

def

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

def

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

def

Subarray.all.{u} {α : Type u} (p : α → Bool)
  (as : Subarray α) : Bool

def

Subarray.allM.{u, w} {α : Type u}
  {m : Type → Type w} [Monad m] (p : α → m Bool)
  (as : Subarray α) : m Bool

def

Subarray.any.{u} {α : Type u} (p : α → Bool)
  (as : Subarray α) : Bool

def

Subarray.anyM.{u, w} {α : Type u}
  {m : Type → Type w} [Monad m] (p : α → m Bool)
  (as : Subarray α) : m Bool

14.16.6. FFI🔗

FFI type

typedef struct {
    lean_object   m_header;
    size_t        m_size;
    size_t        m_capacity;
    lean_object * m_data[];
} lean_array_object;

The representation of arrays in C. See the description of run-time Arrays for more details.

FFI function

bool lean_is_array(lean_object * o)

Returns true if o is an array, or false otherwise.

FFI function

lean_array_object * lean_to_array(lean_object * o)

Performs a runtime check that o is indeed an array. If o is not an array, an assertion fails.

Planned Content

Complete C API for Array

Tracked at issue #158