12.17. 配列（Arrays）🔗

Array 型は要素のシーケンスを表し、シーケンス内の位置によってアクセスすることが可能です。配列は Lean で特別にサポートされています：

配列には要素のリストという観点からその動作を指定する 論理モデル があり、配列に対する各操作の意味を指定します。
動的配列としてコンパイルされたコードに最適化されたランタイム表現があり、Lean のランタイムは配列操作を特別に最適化します。
配列を記述するための配列リテラル構文が存在します。

配列はコンパイルされたコードにおいて、リストや他の配列よりも遥かに効率的です。これは配列が良い局所性を要求しているためです：配列のすべての要素がメモリ上で隣り合っているため、プロセッサのキャッシュを効率的に使うことができます。さらに重要なのは、配列への参照が1つだけであれば、データ構造をコピーしたり割り当てたりするような操作はミューテーションによって実装できるということです。一意な参照が1つしかないような配列を使用する（つまり、 linearly に使用する）Lean コードは、永続的なデータ構造のパフォーマンスオーバーヘッドを回避しつつ、通常の純粋関数型プログラムと同じように便利に書いたり読んだり証明したりすることができます。

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

配列の論理モデルは、要素のリストである1つのフィールドを含む構造体です。これは配列処理関数の特性を低レベルで指定・証明する場合に便利です。

12.17.2. ランタイム表現（Run-Time Representation）🔗

Lean の配列は 動的配列 （dynamic array）であり、定義された容量（たいていすべて使われることはない）を持つ連続メモリのブロックです。配列の要素数が容量より少ない場合、データを再割り当てしたり、移動したりすることなく、新しい項目を末尾に追加できます。スペースに空きの無い配列に項目を追加すると、再割り当てで容量が2倍になります。償却されるオーバーヘッドは配列の大きさに応じて線形に増加します。配列内の値は外部関数インタフェースの節で説明されているように表現されます。

オブジェクトのヘッダに続き、配列は以下を保持します：

サイズ: 現在配列に格納されているオブジェクトの数

容量: 配列に割り当てられたメモリに収まるオブジェクトの数

データ: 配列に格納された値

Lean のランタイムにて多くの配列関数は、オブジェクトヘッダの参照カウントを参照することで、引数に排他アクセスがあるかどうかをチェックします。もし排他アクセスがあり、配列の容量が十分であれば、新しいメモリを確保するのではなく、既存の配列を変更することができます。そうでない場合は、新しい配列を割り当てる必要があります。

12.17.2.1. パフォーマンスについての注記（Performance Notes）🔗

一見普通のコンストラクタと射影のように見えますが、 Array.mk と Array.data はコンパイルされたコードにおいて 配列のサイズに比例した時間 がかかります。これは連結リストと packed array の間の変換を実装する必要があるためで、各要素を訪問する必要があります。

可変配列は非常に効率的なコードを書くために使うことができます。しかし、これは永続性の低いデータ構造です。共有された配列の更新はミューテーションを排除し、配列のサイズに線形な時間を必要とします。パフォーマンスが重要なコードで配列を使用する場合、 linearly に使用されるようにすることが重要です。

12.17.3. 構文（Syntax）🔗

配列リテラルによって、配列がコードで直接記述できるようになります。配列リテラルは式やパターンのコンテキストで使うことができます。

syntax

配列リテラルは #[ で始まり、カンマで区切られた一連の項を含み、] で終わります。

term ::= ...
    | #[term,*]

配列リテラル

配列リテラルは式としてもパターンとしても使用できます。

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

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

さらに、部分配列は以下の構文を使って取り出すことができます：

syntax

開始インデックスの後にコロンを付けると、開始インデックス（を含み）以降の値を含む部分配列が構成されます：

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

開始インデックスと終了インデックスを指定すると、開始インデックス（含む）から終了インデックス（含まない）までの値を含む部分配列が構成されます：

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

部分配列の構文

配列 ten は0から始まる10個の自然数を含みます。

def ten : Array Nat :=
  .range 10

ten の後半を表す部分配列は、部分配列構文を使って作ることができます：

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

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

同様に、2番目から5番目までを含む部分配列は終了点を設けることで構築できます：

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

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

部分配列は単にベースとなる配列の開始と終了のインデックスを格納するだけであるため、配列そのものを復元することができます：

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

true

12.17.4. API リファレンス（API Reference）🔗

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

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

12.17.4.3. 検索（Lookups）

def

Array.extract.{u_1} {α : Type u_1}
    (as : Array α) (start stop : Nat) : 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.get.{u} {α : Type u} (a : Array α)
    (i : Nat) (h : i < a.size) : α

Access an element from an array without needing a runtime bounds checks, using a Nat index and a proof that it is in bounds.

This function does not use get_elem_tactic to automatically find the proof that the index is in bounds. This is because the tactic itself needs to look up values in arrays. Use the indexing notation a[i] instead.

def

Array.get?.{u} {α : Type u} (a : Array α)
    (i : Nat) : Option α

def

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

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

Access an element from an array, or panic 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 α

def

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

def

Array.back.{u_1} {α : Type u_1} [Inhabited α]
    (a : Array α) : α

def

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

12.17.4.4. 別の型への変換（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.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 α

12.17.4.5. 配列の変更（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 α

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.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.swap!.{u_1} {α : Type u_1} (a : Array α)
    (i j : Nat) : Array α

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.setD.{u_1} {α : Type u_1} (a : Array α)
    (i : Nat) (v : α) : Array α

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.insertAt.{u_1} {α : Type u_1}
    (as : Array α) (i : Nat) (a : α)
    : autoParam (i ≤ as.size) _auto✝ → Array α

def

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

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.

def

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

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 α

12.17.4.6. 配列のソート（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

12.17.4.7. 反復（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'

12.17.4.8. 要素の変換（Transformation）

def

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

def

Array.concatMapM.{u_1, u_2, u_3} {α : Type u_1}
    {m : Type u_2 → Type u_3} {β : Type u_2}
    [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} (as : Array α)
    (bs : Array β) (f : α → β → γ) : Array γ

def

Array.zipWithIndex.{u} {α : Type u}
    (arr : Array α) : 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 : Fin 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 : Fin as.size → α → m β)
    : m (Array β)

Variant of mapIdxM which receives the index as a Fin 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 β)

def

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

12.17.4.9. フィルタ（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.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)

12.17.4.10. 分割（Partitioning）

def

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

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.

12.17.4.11. 要素についての述語（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.indexOf?.{u} {α : Type u} [BEq α]
    (a : Array α) (v : α) : Option (Fin a.size)

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 α) : Option Nat

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 α) : β

12.17.4.12. 比較（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 α.

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

12.17.4.14. 証明の自動化（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.

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

12.17.5.1. サイズ（Size）

def

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

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

12.17.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₀ : α) : α

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

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

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

C における配列表現。詳しくはランタイムにおける Array についての説明を参照してください。

FFI function

bool lean_is_array(lean_object * o)

o が配列であれば true を、そうでない場合は false を返します。

FFI function

lean_array_object * lean_to_array(lean_object * o)

o が本当に配列であるかどうかを実行時にチェックします。o が配列でない場合、アサートが失敗します。

Planned Content

Complete C API for Array

Tracked at issue #158