Array 类型表示元素序列，可以通过其在序列中的位置进行访问。
Lean 对数组提供了专门支持：
它有一个逻辑模型，用元素列表来规定其行为，从而给出各个数组操作的含义。
它在编译后的代码中有一种经过优化的运行时表示，即 动态数组，Lean 运行时还会专门优化数组操作。
可以使用 数组字面量语法 来书写数组。
在编译后的代码中，数组可以比列表或其他序列高效得多。 这部分是因为它具有良好的局部性：序列中的所有元素都在内存中彼此相邻，因此处理器缓存可以被高效利用。 更重要的是，如果一个数组只有唯一引用，那么原本需要复制或分配数据结构的操作就可以通过原地修改来实现。 当 Lean 代码以始终只有唯一引用的方式使用数组时（也就是 线性地 使用它），便能避免持久化数据结构的性能开销，同时依旧像普通纯函数式程序一样易于编写、阅读与证明性质。
Array α 是动态数组 的类型，其中元素来自 α。该类型在运行时有特殊支持。
数组在不共享时性能最佳。只要对数组的引用不超过一次，所有更新都将_破坏性地_执行。这导致性能与命令式编程语言中的可变数组相当。
数组有大小和容量。大小是数组中存在的元素数量，而容量是当前为元素分配的内存量。可以通过 Array.size 访问大小，但无法从Lean 代码中观察到容量。 Array.emptyWithCapacity n 创建一个等于 #[] 的数组，但内部分配了一个容量为 n 的数组。当大小超过容量时，需要分配以扩大数组。
从证明的角度来看，Array α 只是 List α 的包装。
构造子
Array.mk.{u}
数组的逻辑模型是一个只有单个字段的结构体，该字段是元素列表。 这使得在较低层次上规定和证明数组处理函数的性质时更加方便。
Lean 的数组是 动态数组：它们是一段具有既定容量的连续内存块，通常其中不会全部被占用。 只要数组中的元素个数小于容量，就可以在末尾追加新元素，而无需重新分配或移动数据。 向没有剩余空间的数组中添加元素时，会触发一次将容量翻倍的重新分配。 其摊还开销与数组大小呈线性关系。 数组中的值按 外部函数接口一节所述的方式表示。
在对象头之后，数组包含：
当前存储在数组中的对象个数
为数组分配的内存中可容纳的对象个数
数组中的值
Lean 运行时中的许多数组函数都会通过查看对象头中的引用计数，来检查自己是否独占其参数。 如果是，并且数组容量足够，那么就可以直接修改现有数组，而无需分配新的内存。 否则，就必须分配一个新数组。
尽管 Array.mk 和 Array.toList 看起来只是普通的构造子与投影，但在编译后的代码中，它们都需要 与数组大小成线性关系的时间。
这是因为在链表与紧凑数组之间转换时，必然需要访问每一个元素。
可变数组可用于编写非常高效的代码。 不过，它们并不是好的持久化数据结构。 更新共享数组时无法使用原地修改，并且需要耗费与数组大小成线性关系的时间。 在性能关键的代码中使用数组时，务必确保它们是 线性地 使用的。
数组字面量允许直接在代码中书写数组。 它们既可用于表达式上下文，也可用于模式上下文。
数组字面量以 #[ 开始，包含一串以逗号分隔的项，并以 ] 结束。
term ::= ...
| 此外，还可以用下列语法提取 子数组：
起始下标后跟一个冒号，会构造出一个子数组，包含从起始下标开始（含该位置）直到末尾的值：
term ::= ...
| 同时提供起始与结束下标时，会构造出一个子数组，包含从起始下标（含）到结束下标（不含）的值：
term ::= ...
|
构造一个新的空数组，初始容量为 c。
构造一个数组，其中包含从 0 到 n 的所有数字（不包括）。
示例：
Array.range 5 := #[0, 1, 2, 3, 4]
Array.range 0 := #[]
Array.range 1 := #[0]
构造一个大小为 size 的数字数组，从 start 开始，每个元素增加 step。
换句话说，Array.range' start size step 是 #[start, start+step, ..., start+(len-1)*step]。
示例：
Array.range' 0 3 (step := 1) = #[0, 1, 2]
Array.range' 0 3 (step := 2) = #[0, 2, 4]
Array.range' 0 4 (step := 2) = #[0, 2, 4, 6]
Array.range' 3 4 (step := 2) = #[3, 5, 7, 9]
按顺序返回 Fin n 中所有元素的数组，从 0 开始。
示例：
Array.finRange 0 = (#[] : Array (Fin 0))
Array.finRange 2 = (#[0, 1] : Array (Fin 2))
通过按顺序将 f 应用于每个潜在索引（从 0 开始）来创建数组。
示例：
Array.ofFn (n := 3) toString = #["0", "1", "2"]
Array.ofFn (fun i => #["red", "green", "blue"].get i.val i.isLt) = #["red", "green", "blue"]
创建一个数组，其中 n 个元素均为 v。
对应的List函数为List.replicate。
示例：
Array.replicate 2 true = #[true, true]
Array.replicate 3 () = #[(), (), ()]
Array.replicate 0 "anything" = #[]
添加两个数组。通常通过 ++ 运算符使用。
追加数组所需的时间与第二个数组的长度成正比。
示例：
#[1, 2, 3] ++ #[4, 5] = #[1, 2, 3, 4, 5]。
#[] ++ #[4, 5] = #[4, 5]。
#[1, 2, 3] ++ #[] = #[1, 2, 3]。
追加一个数组和一个列表。
花费的时间与列表的长度成正比。
示例：
#[1, 2, 3].appendList [4, 5] = #[1, 2, 3, 4, 5]。
#[].appendList [4, 5] = #[4, 5]。
#[1, 2, 3].appendList [] = #[1, 2, 3]。
获取数组中存储的元素数。
这是一个缓存值，因此要访问的是O(1)。为数组分配的空间（称为“容量”）至少与其大小一样大，但也可能更大。数组的容量是Lean 代码无法观察到的内部细节。
以平台本机无符号整数形式返回数组的大小。
这是 Array.size 的低级版本，直接查询运行时系统的数组表示。虽然这无法证明，但 Array.usize 始终返回数组的确切大小，因为该实现仅支持大小小于 USize.size 的数组。
将数组添加到列表前面。数组的元素位于结果列表的开头。
相当于as.toList ++ l。
示例：
#[1, 2].toListAppend [3, 4] = [1, 2, 3, 4]
#[1, 2].toListAppend [] = [1, 2]
#[].toListAppend [3, 4, 5] = [3, 4, 5]
将数组转换为向量。结果向量的大小就是数组的大小。
返回具有给定边界的数组的子数组。
如果 start 或 stop 不是子数组的有效边界，则它们将被限制为数组的大小。此外，起始索引被限制到结束索引。
分配一个包含子数组内容的新数组。
删除第一个满足谓词 p 的元素。如果没有元素满足 p，则返回未修改的数组。
此函数在最坏情况下需要 O(n) 时间，因为它会向后移动所有后面的元素。
示例：
#["red", "green", "", "blue"].eraseP (·.isEmpty) = #["red", "green", "blue"]
#["red", "green", "", "blue", ""].eraseP (·.isEmpty) = #["red", "green", "blue", ""]
#["red", "green", "blue"].eraseP (·.length % 2 == 0) = #["red", "green"]
#["red", "green", "blue"].eraseP (fun _ => true) = #["green", "blue"]
从数组中删除给定索引处的元素。如果索引越界，则会触发 panic。
此函数需要最坏情况下的 O(n) 时间，因为它会将大于 i 的位置处的所有元素后移。
从数组中删除给定索引处的元素。如果索引越界，则不执行任何操作。
此函数需要最坏情况下的 O(n) 时间，因为它会将大于 i 的位置处的所有元素后移。
示例：
#["apple", "pear", "orange"].eraseIdxIfInBounds 0 = #["pear", "orange"]
#["apple", "pear", "orange"].eraseIdxIfInBounds 1 = #["apple", "orange"]
#["apple", "pear", "orange"].eraseIdxIfInBounds 2 = #["apple", "pear"]
#["apple", "pear", "orange"].eraseIdxIfInBounds 3 = #["apple", "pear", "orange"]
#["apple", "pear", "orange"].eraseIdxIfInBounds 5 = #["apple", "pear", "orange"]
交换数组的两个元素。当对数组的引用是唯一的时，修改就地执行。
示例：
#["red", "green", "blue", "brown"].swap 0 3 = #["brown", "green", "blue", "red"]
#["red", "green", "blue", "brown"].swap 0 2 = #["blue", "green", "red", "brown"]
#["red", "green", "blue", "brown"].swap 1 2 = #["red", "blue", "green", "brown"]
#["red", "green", "blue", "brown"].swap 3 0 = #["brown", "green", "blue", "red"]
交换数组的两个元素，如果任一索引超出范围，则返回数组不变。当对数组的引用是唯一的时，修改就地执行。
示例：
#["red", "green", "blue", "brown"].swapIfInBounds 0 3 = #["brown", "green", "blue", "red"]
#["red", "green", "blue", "brown"].swapIfInBounds 0 2 = #["blue", "green", "red", "brown"]
#["red", "green", "blue", "brown"].swapIfInBounds 1 2 = #["red", "blue", "green", "brown"]
#["red", "green", "blue", "brown"].swapIfInBounds 0 4 = #["red", "green", "blue", "brown"]
#["red", "green", "blue", "brown"].swapIfInBounds 9 2 = #["red", "green", "blue", "brown"]
在数组中设置一个元素，或者如果索引越界则触发 panic。
如果调用时 a 的引用计数为 1，这将破坏性地执行更新。
替换数组中提供的索引处的元素。如果索引越界，则返回未修改的数组。
如果没有其他引用，则该数组将被就地修改。
示例：
#[0, 1, 2].setIfInBounds 1 5 = #[0, 5, 2]
#["orange", "apple"].setIfInBounds 1 "grape" = #["orange", "grape"]
#["orange", "apple"].setIfInBounds 5 "grape" = #["orange", "apple"]
Array.modifyM.{u, u_1} {α : Type u} {m : Type u → Type u_1} [Monad m] (xs : Array α) (i : Nat) (f : α → m α) : m (Array α)Array.modifyM.{u, u_1} {α : Type u} {m : Type u → Type u_1} [Monad m] (xs : Array α) (i : Nat) (f : α → m α) : m (Array α)
将给定索引处的元素（如果存在）替换为对其应用一元函数 f 的结果。如果索引无效，则返回未修改的数组，并且不会调用 f。
示例：
#eval #[1, 2, 3, 4].modifyM 2 fun x => do
IO.println s!"It was {x}"
return x * 10
It was 3#[1, 2, 30, 4]#eval #[1, 2, 3, 4].modifyM 6 fun x => do
IO.println s!"It was {x}"
return x * 10
#[1, 2, 3, 4]将元素插入到数组中指定索引处。如果索引大于数组的大小，则返回未修改的数组。
换句话说，新元素被插入到数组 as 中前 i 个元素之后；此数组即 as。
此函数在最坏情况下需要 O(n) 时间，因为它必须将插入的元素交换到位。
示例：
将元素插入到数组中指定索引处。如果索引大于数组的大小，则会触发 panic。
换句话说，新元素被插入到数组 as 中前 i 个元素之后；此数组即 as。
此函数在最坏情况下需要 O(n) 时间，因为它必须将插入的元素交换到位。 Array.insertIdx 和 Array.insertIdxIfInBounds 是更安全的替代品。
示例：
#["tues", "thur", "sat"].insertIdx! 1 "wed" = #["tues", "wed", "thur", "sat"]
#["tues", "thur", "sat"].insertIdx! 2 "wed" = #["tues", "thur", "wed", "sat"]
#["tues", "thur", "sat"].insertIdx! 3 "wed" = #["tues", "thur", "sat", "wed"]
将元素插入到数组中指定索引处。如果索引大于数组的大小，则返回未修改的数组。
换句话说，新元素被插入到数组 as 中前 i 个元素之后；此数组即 as。
此函数在最坏情况下需要 O(n) 时间，因为它必须将插入的元素交换到位。
示例：
#["tues", "thur", "sat"].insertIdxIfInBounds 1 "wed" = #["tues", "wed", "thur", "sat"]
#["tues", "thur", "sat"].insertIdxIfInBounds 2 "wed" = #["tues", "thur", "wed", "sat"]
#["tues", "thur", "sat"].insertIdxIfInBounds 3 "wed" = #["tues", "thur", "sat", "wed"]
#["tues", "thur", "sat"].insertIdxIfInBounds 4 "wed" = #["tues", "thur", "sat"]
返回一个新数组，其中包含 as 中偶数索引处的元素，从索引 0 处的元素开始。
示例：
#[0, 1, 2, 3, 4].getEvenElems = #[0, 2, 4]
#[1, 2, 3, 4].getEvenElems = #[1, 3]
#["red", "green", "blue"].getEvenElems = #["red", "blue"]
(#[] : Array String).getEvenElems = #[]
就地快速排序。
qsort as lt lo hi 对子数组 as[lo...=hi] 进行就地排序，并使用 lt 比较元素。
Array.insertionSort.{u_1} {α : Type u_1} (xs : Array α) (lt : α → α → Bool := by exact (· < ·)) : Array αArray.insertionSort.{u_1} {α : Type u_1} (xs : Array α) (lt : α → α → Bool := by exact (· < ·)) : Array α
使用插入排序对数组进行排序。
可选参数 lt 指定排序谓词。它默认为 LT.lt，它必须是可判定的才能用于排序。
将一个元素插入到已排序的数组中，以便对结果数组进行排序。如果该元素已存在于数组中，则不会插入该元素。
排序谓词 lt 应该是元素的总顺序，并且数组 as 应相对于 lt 进行排序。
Array.binInsertM 是一个更通用的运算符，除了在 monad 中运行之外，还可以更好地控制重复元素的处理。
示例：
将元素 k 插入已排序数组 as 中，以便对结果数组进行排序。
排序谓词 lt 应该是元素的总顺序，并且数组 as 应相对于 lt 进行排序。
如果 lt 等于 k 的元素已存在于 as 中，则 merge 将应用于现有元素以确定结果数组中该位置的值。如果不存在等于 k 的元素，则使用 add 来确定要插入的值。
二分查找与 k 等效的元素，搜索对象是排序数组 as。如果找到，则返回数组中的元素，否则返回 none。
数组as必须根据比较运算符lt进行排序，这应该是全序。
可选参数 lo 和 hi 确定要搜索的数组索引的区域。两者都是包容性的，并且默认搜索整个数组。
返回从给定索引开始的给定数组的有限迭代器。迭代器按顺序生成数组的元素，然后终止。
该迭代器的单子版本是 Array.iterFromIdxM。
终止属性：
Finite 实例：始终
Productive 实例：始终
Array.iterFromIdxM.{w, w'} {α : Type w} (array : Array α) (m : Type w → Type w') (pos : Nat) [Pure m] : Std.IterM m αArray.iterFromIdxM.{w, w'} {α : Type w} (array : Array α) (m : Type w → Type w') (pos : Nat) [Pure m] : Std.IterM m α
返回从给定索引开始的给定数组的有限一元迭代器。迭代器按顺序生成数组的元素，然后终止。
该迭代器的纯净版本是Array.iterFromIdx。
终止属性：
Finite 实例：始终
Productive 实例：始终
Array.foldr.{u, v} {α : Type u} {β : Type v} (f : α → β → β) (init : β) (as : Array α) (start : Nat := as.size) (stop : Nat := 0) : βArray.foldr.{u, v} {α : Type u} {β : Type v} (f : α → β → β) (init : β) (as : Array α) (start : Nat := as.size) (stop : Nat := 0) : β
从右侧开始在数组上折叠一元函数，累积以 init 开头的值。使用 f 将累积值与列表中的每个元素按相反顺序组合。
可选参数 start 和 stop 控制要折叠的阵列区域。折叠从start（不包括）到stop（包括）进行，因此除非start > stop，否则不会发生折叠。默认情况下，整个数组是折叠的。
示例：
example [Monad m] (f : α → β → m β) :
Array.foldrM (m := m) f x₀ #[a, b, c] = (do
let x₁ ← f c x₀
let x₂ ← f b x₁
let x₃ ← f a x₂
pure x₃)
:= by rfl
example [Monad m] (f : α → β → m β) :
Array.foldrM (m := m) f x₀ #[a, b, c] (start := 2) = (do
let x₁ ← f b x₀
let x₂ ← f a x₁
pure x₂)
:= by rfl
Array.foldl.{u, v} {α : Type u} {β : Type v} (f : β → α → β) (init : β) (as : Array α) (start : Nat := 0) (stop : Nat := as.size) : βArray.foldl.{u, v} {α : Type u} {β : Type v} (f : β → α → β) (init : β) (as : Array α) (start : Nat := 0) (stop : Nat := as.size) : β
将一元函数从左侧折叠到列表上，累积以 init 开头的值。使用 f 将累加值按顺序与列表中的每个元素组合。
可选参数 start 和 stop 控制要折叠的阵列区域。折叠从start（包含）到stop（不包含）进行，因此除非start < stop，否则不会发生折叠。默认情况下，整个数组是折叠的。
示例：
example [Monad m] (f : α → β → m α) :
Array.foldlM (m := m) f x₀ #[a, b, c] = (do
let x₁ ← f x₀ a
let x₂ ← f x₁ b
let x₃ ← f x₂ c
pure x₃)
:= by rfl
example [Monad m] (f : α → β → m α) :
Array.foldlM (m := m) f x₀ #[a, b, c] (start := 1) = (do
let x₁ ← f x₀ b
let x₂ ← f x₁ c
pure x₂)
:= by rfl
按顺序将一元操作 f 应用于数组的每个元素。
可选参数 start 和 stop 控制应应用 f 的数组区域。迭代从start（包含）到stop（不包含）进行，因此不会调用f，除非start < stop。默认情况下，使用整个数组。
以相反的顺序从右到左将一元操作 f 应用于数组的每个元素。
可选参数 start 和 stop 控制应应用 f 的数组区域。迭代从start（不包括）到stop（包括），因此不会调用f，除非start > stop。默认情况下，使用整个数组。
Array.firstM.{u, v, w} {β : Type v} {α : Type u} {m : Type v → Type w} [Alternative m] (f : α → m β) (as : Array α) : m βArray.firstM.{u, v, w} {β : Type v} {α : Type u} {m : Type v → Type w} [Alternative m] (f : α → m β) (as : Array α) : m β
在阵列上映射 f 并使用 <|> 收集结果。数组末尾的结果是 failure。
示例：
#[[], [1, 2], [], [2]].firstM List.head? = some 1
#[[], [], []].firstM List.head? = none
#[].firstM List.head? = none
将函数应用于数组的每个元素，返回结果数组。该函数是单态的：要求返回相同类型的值。内部实现使用指针相等，并且如果每个函数调用的结果与其参数指针相等，则不会分配新数组。
Array.mapM.{u, v, w} {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m β) (as : Array α) : m (Array β)Array.mapM.{u, v, w} {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m β) (as : Array α) : m (Array β)
将一元操作 f 从左到右应用于数组中的每个元素，并返回结果数组。
将一元操作 f 从左到右应用于数组中的每个元素，并返回结果数组。此外，结果数组的类型保证它包含与输入数组相同数量的元素。
Array.mapMonoM.{u_1, u_2} {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] (as : Array α) (f : α → m α) : m (Array α)Array.mapMonoM.{u_1, u_2} {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] (as : Array α) (f : α → m α) : m (Array α)
将一元函数应用于数组的每个元素，返回结果数组。该函数是单态的：要求返回相同类型的值。内部实现使用指针相等，并且如果每个函数调用的结果与其参数指针相等，则不会分配新数组。
Array.mapIdxM.{u, v, w} {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : Nat → α → m β) (as : Array α) : m (Array β)Array.mapIdxM.{u, v, w} {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : Nat → α → m β) (as : Array α) : m (Array β)
将一元操作 f 从左到右应用于数组中的每个元素以及元素的索引。返回结果数组。
将函数应用于数组的每个元素以及找到该元素的索引，返回结果数组。除了索引之外，该函数还提供了索引有效的证明。
Array.mapIdx 是一个变体，它不向函数提供索引有效的证据。
将一元操作 f 应用于数组中的每个元素，以及元素的索引和索引在边界内的证明（从左到右）。返回结果数组。
应用一个将数组返回到数组的每个元素的函数。附加结果数组。
示例：
#[2, 3, 2].flatMap Array.range = #[0, 1, 0, 1, 2, 0, 1]
#[['a', 'b'], ['c', 'd', 'e']].flatMap List.toArray = #['a', 'b', 'c', 'd', 'e']
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 β)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 β)
应用一个单子函数，该函数从左到右将数组返回到数组的每个元素。附加结果数组。
Array.zipWith.{u, u_1, u_2} {α : Type u} {β : Type u_1} {γ : Type u_2} (f : α → β → γ) (as : Array α) (bs : Array β) : Array γArray.zipWith.{u, u_1, u_2} {α : Type u} {β : Type u_1} {γ : Type u_2} (f : α → β → γ) (as : Array α) (bs : Array β) : Array γ
返回 as 中的元素数组，其中 p 返回 true。
仅考虑从 start（含）到 stop（不含）的元素。该范围之外的元素将被丢弃。默认情况下，考虑整个数组。
示例：
#[1, 2, 5, 2, 7, 7].filter (· > 2) = #[5, 7, 7]
#[1, 2, 5, 2, 7, 7].filter (fun _ => true) = #[1, 2, 5, 2, 7, 7]
#[1, 2, 5, 2, 7, 7].filter (· > 2) (start := 3) = #[7, 7]
#[1, 2, 5, 2, 7, 7].filter (fun _ => true) (start := 3) = #[2, 7, 7]
#[1, 2, 5, 2, 7, 7].filter (fun _ => true) (stop := 3) = #[1, 2, 5]
按从左到右的顺序将一元谓词 p 应用于数组中的每个元素，并返回 p 返回 true 的元素数组。
仅考虑从 start（含）到 stop（不含）的元素。该范围之外的元素将被丢弃。默认情况下，检查整个数组。
例子：
#eval #[1, 2, 5, 2, 7, 7].filterM fun x => do
IO.println s!"Checking {x}"
return x < 3
Checking 1
Checking 2
Checking 5
Checking 2
Checking 7
Checking 7#[1, 2, 2]
以相反的顺序（从右到左）对数组中的每个元素应用一元谓词 p，并返回 p 返回 true 的那些元素。返回列表中元素的顺序与输入列表中的顺序相同。
仅考虑从 start（不包括）到 stop（包括）的元素。该范围之外的元素将被丢弃。由于按相反顺序检查数组，因此仅在 start > stop 时检查元素。默认情况下，考虑整个数组。
例子：
#eval #[1, 2, 5, 2, 7, 7].filterRevM fun x => do
IO.println s!"Checking {x}"
return x < 3
Checking 7
Checking 7
Checking 2
Checking 5
Checking 2
Checking 1#[1, 2, 2]
应用一元函数，该函数将 Option 返回到数组的每个元素，并收集非 none 值。
仅考虑从 start（含）到 stop（不含）的元素。该范围之外的元素将被丢弃。默认情况下，考虑整个数组。
例子：
#eval #[1, 2, 5, 2, 7, 7].filterMapM fun x => do
IO.println s!"Examining {x}"
if x > 2 then return some (2 * x)
else return none
Examining 1
Examining 2
Examining 5
Examining 2
Examining 7
Examining 7#[10, 14, 14]Array.filterSepElemsM {m : Type → Type} [Monad m] (a : Array Lean.Syntax) (p : Lean.Syntax → m Bool) : m (Array Lean.Syntax)Array.filterSepElemsM {m : Type → Type} [Monad m] (a : Array Lean.Syntax) (p : Lean.Syntax → m Bool) : m (Array Lean.Syntax)
过滤语法数组，将所有其他元素视为分隔符，而不是使用一元谓词 p 进行测试的元素。生成的数组包含 p 返回 true 的测试元素，并由相应的分隔符元素分隔。
Array.groupByKey.{u, v} {α : Type u} {β : Type v} [BEq α] [Hashable α] (key : β → α) (xs : Array β) : Std.HashMap α (Array β)Array.groupByKey.{u, v} {α : Type u} {β : Type v} [BEq α] [Hashable α] (key : β → α) (xs : Array β) : Std.HashMap α (Array β)
对数组 xs 的元素按函数 key 分组，返回一个哈希映射，其中每个组与其键相关联。组保留 xs 中元素的相对顺序。
例子：
#eval #[0, 1, 2, 3, 4, 5, 6].groupByKey (· % 2)
Std.HashMap.ofList [(0, #[0, 2, 4, 6]), (1, #[1, 3, 5])]
检查 a 是否是 as 的元素，使用 == 进行元素比较。
Array.elem 是一个同义词，它采用数组之前的元素。
示例：
Array.contains #[1, 4, 2, 3, 3, 7] 5 = false
检查 a 是否是 as 的元素，使用 == 进行元素比较。
Array.contains 是一个同义词，它将数组放在元素之前。
出于验证目的，Array.elem 简化为 Array.contains。
例子：
Array.elem 3 #[1, 4, 2, 3, 3, 7] = true
Array.elem 5 #[1, 4, 2, 3, 3, 7] = false
返回 p 返回 true 的第一个元素的索引，如果没有这样的元素，则返回 none。该索引以 Fin 形式返回，这保证它在范围内。
示例：
#[7, 6, 5, 8, 1, 2, 6].findFinIdx? (· < 5) = some (4 : Fin 7)
#[7, 6, 5, 8, 1, 2, 6].findFinIdx? (· < 1) = none
Array.findM?.{u_1} {m : Type → Type u_1} {α : Type} [Monad m] (p : α → m Bool) (as : Array α) : m (Option α)Array.findM?.{u_1} {m : Type → Type u_1} {α : Type} [Monad m] (p : α → m Bool) (as : Array α) : m (Option α)
Array.findRevM?.{w} {α : Type} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Array α) : m (Option α)Array.findRevM?.{w} {α : Type} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Array α) : m (Option α)
Array.findSome!.{u, v} {α : Type u} {β : Type v} [Inhabited β] (f : α → Option β) (xs : Array α) : βArray.findSome!.{u, v} {α : Type u} {β : Type v} [Inhabited β] (f : α → Option β) (xs : Array α) : β
Array.findSomeM?.{u, v, w} {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m (Option β)) (as : Array α) : m (Option β)Array.findSomeM?.{u, v, w} {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m (Option β)) (as : Array α) : m (Option β)
按顺序返回第一个非 none 结果，它来自把单子函数 f 应用于数组的各元素。返回值为 none 的条件是：f 对所有元素返回 none。
例子：
#eval #[7, 6, 5, 8, 1, 2, 6].findSomeM? fun i => do
if i < 5 then
return some (i * 10)
if i ≤ 6 then
IO.println s!"Almost! {i}"
return none
Almost! 6
Almost! 5some 10Array.findSomeRevM?.{u, v, w} {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m (Option β)) (as : Array α) : m (Option β)Array.findSomeRevM?.{u, v, w} {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m (Option β)) (as : Array α) : m (Option β)
返回第一个非 none 结果，它来自将单子函数 f 按相反顺序（从右到左）应用于数组的各元素。一旦找到非 none 结果，就不再检查其他元素。返回 none，如果 f 对数组的所有元素都返回 none。
示例：
#eval #[1, 2, 0, -4, 1].findSomeRevM? (m := Except String) fun x => do
if x = 0 then throw "Zero!"
else if x < 0 then return (some x)
else return none
Except.ok (some (-4))#eval #[1, 2, 0, 4, 1].findSomeRevM? (m := Except String) fun x => do
if x = 0 then throw "Zero!"
else if x < 0 then return (some x)
else return none
Except.error "Zero!"
返回值为 true 的条件是：as 是 bs 的前缀，否则返回 false。
示例：
#[0, 1, 2].isPrefixOf #[0, 1, 2, 3] = true
#[0, 1, 2].isPrefixOf #[0, 1, 2] = true
#[0, 1, 2].isPrefixOf #[0, 1] = false
#[].isPrefixOf #[0, 1] = true
Array.lex.{u_1} {α : Type u_1} [BEq α] (as bs : Array α) (lt : α → α → Bool := by exact (· < ·)) : BoolArray.lex.{u_1} {α : Type u_1} [BEq α] (as bs : Array α) (lt : α → α → Bool := by exact (· < ·)) : Bool
按字典顺序比较数组及其元素上的比较 lt。
具体来说，如果 Array.lex as bs lt 为真，则
bs 大于 as 并且 as 通过 == 成对等效于 bs 的初始段，
或者
存在索引 i，例如 lt as[i] bs[i]，并且对于所有 j < i，as[j] == bs[j]。
将各个证明“附加”到满足谓词 P 的值数组，返回相应子类型 { x // P x } 中的元素数组。
O(1)。
通过忘记它们满足谓词，将子类型中的术语数组映射到类型中的相应术语。
这是 Array.attachWith 的逆值，也是 xs.map (·.val) 的同义词。
大多数情况下，用户不需要这样做。它是由诸如 map_subtype 之类的引理作为中间步骤引入的，并且理想情况下随后由 unattach_attach 进行简化。
该函数通常由 Lean 自动插入，作为证明终止性时的中间步骤，很少在代码中显式使用。精化良基递归定义时会引入它。如果在证明状态中遇到此函数，通常应使用策略 simp [Array.unattach, -Array.map_subtype]。
Array.pmap.{u_1, u_2} {α : Type u_1} {β : Type u_2} {P : α → Prop} (f : (a : α) → P a → β) (xs : Array α) (H : ∀ (a : α), a ∈ xs → P a) : Array βArray.pmap.{u_1, u_2} {α : Type u_1} {β : Type u_2} {P : α → Prop} (f : (a : α) → P a → β) (xs : Array α) (H : ∀ (a : α), a ∈ xs → P a) : Array β
将部分定义的函数（定义于 α 中满足谓词 P 的项上）映射到数组 xs : Array α，并给出 xs 的每个元素实际上满足 P 的证明。
Array.pmap，以“部分映射”命名，相当于此类部分函数的 Array.map。
类型 Subarray α 是 Std.Slice α 的缩写。
这意味着，除了本节中的运算符外，还可以使用泛化字段记号来调用 Std.Slice 命名空间中的函数，例如 Std.Slice.foldl。
某些底层数组的区域。
子数组包含一个数组以及感兴趣区域的起始索引和结束索引。子数组可用于避免复制或分配空间，同时比手动跟踪边界更方便。感兴趣区域由大于或等于 start 且严格小于 stop 的每个索引组成。
空子数组。
这个空子数组由一个空数组支持。
底层数组。
感兴趣区域的起始索引（含）。
感兴趣区域的结束索引（不包括）。
起始索引不晚于结束索引。
结束索引是排他的。如果起始索引和结束索引相等，则子数组为空。
删除子数组的第一个 i 元素。如果元素数量为 i 或更少，则生成的子数组为空。
仅保留子数组的前 i 元素。如果元素数量为 i 或更少，则生成的子数组为空。
如果可能的话，通过增加其起始索引来缩小子数组，否则返回原样。
示例：
#[1,2,3].toSubarray.popFront.toArray = #[2, 3]
#[1,2,3].toSubarray.popFront.popFront.toArray = #[3]
#[1,2,3].toSubarray.popFront.popFront.popFront.toArray = #[]
#[1,2,3].toSubarray.popFront.popFront.popFront.popFront.toArray = #[]
从子数组中提取一个元素。
索引是相对于子数组的开头，而不是相对于底层数组。
从子数组中提取元素，或者当索引越界时返回默认值 v₀。
索引是相对于子数组的开头和结尾，而不是相对于底层数组。
在子数组中的元素上从右向左折叠操作。
β 类型的累加器的构造方法是从 init 开始，依次将子数组的每个元素与当前累加器值相结合，从末尾移动到开头。
示例：
#["red", "green", "blue"].toSubarray.foldr (·.length + ·) 0 = 12
#["red", "green", "blue"].toSubarray.popFront.foldr (·.length + ·) 0 = 9
Subarray.foldrM.{u, v, w} {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → β → m β) (init : β) (as : Subarray α) : m βSubarray.foldrM.{u, v, w} {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → β → m β) (init : β) (as : Subarray α) : m β
在子数组中的元素上从右向左折叠一元运算。
β 类型的累加器是通过以下方式构造的：从 init 开始，依次将子数组的每个元素与当前累加器值进行一元组合，从末尾移动到开头。所讨论的单子可能允许提前终止或重复。
示例：
#eval #["red", "green", "blue"].toSubarray.foldrM (init := "") fun x acc => do
let l ← Option.guard (· ≠ 0) x.length
return s!"{acc}({l}){x} "
some "(4)blue (5)green (3)red "#eval #["red", "green", "blue"].toSubarray.foldrM (init := 0) fun x acc => do
let l ← Option.guard (· ≠ 5) x.length
return s!"{acc}({l}){x} "
noneSubarray.forM.{u, v, w} {α : Type u} {m : Type v → Type w} [Monad m] (f : α → m PUnit) (as : Subarray α) : m PUnitSubarray.forM.{u, v, w} {α : Type u} {m : Type v → Type w} [Monad m] (f : α → m PUnit) (as : Subarray α) : m PUnit
对子数组的每个元素运行一元操作。
从最低索引开始处理元素并向上移动。
Subarray.forRevM.{u, v, w} {α : Type u} {m : Type v → Type w} [Monad m] (f : α → m PUnit) (as : Subarray α) : m PUnitSubarray.forRevM.{u, v, w} {α : Type u} {m : Type v → Type w} [Monad m] (f : α → m PUnit) (as : Subarray α) : m PUnit
以相反的顺序对子数组的每个元素运行一元操作。
从最高索引开始处理元素并向下移动。
Subarray.forIn.{v, w, u} {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (s : Subarray α) (b : β) (f : α → β → m (ForInStep β)) : m βSubarray.forIn.{v, w, u} {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (s : Subarray α) (b : β) (f : α → β → m (ForInStep β)) : m β
ForIn.forIn 针对 Subarray 的实现，使其可用于 for 循环的 do 记法。
使用布尔谓词以相反顺序测试子数组中的每个元素，在满足谓词的第一个元素处停止。返回满足谓词的元素，如果没有元素满足谓词，则返回 none。
示例：
#["red", "green", "blue"].toSubarray.findRev? (·.length ≠ 4) = some "green"
#["red", "green", "blue"].toSubarray.findRev? (fun _ => true) = some "blue"
#["red", "green", "blue"].toSubarray 0 0 |>.findRev? (fun _ => true) = none
Subarray.findRevM?.{w} {α : Type} {m : Type → Type w} [Monad m] (as : Subarray α) (p : α → m Bool) : m (Option α)Subarray.findRevM?.{w} {α : Type} {m : Type → Type w} [Monad m] (as : Subarray α) (p : α → m Bool) : m (Option α)
以相反的顺序将一元布尔谓词应用于子数组中的每个元素，在满足谓词的第一个元素处停止。返回满足谓词的元素，如果没有元素满足它，则返回 none。
例子：
#eval #["red", "green", "blue"].toSubarray.findRevM? fun x => do
IO.println x
return (x.length = 5)
blue
greensome 5Subarray.findSomeRevM?.{u, v, w} {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Subarray α) (f : α → m (Option β)) : m (Option β)Subarray.findSomeRevM?.{u, v, w} {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Subarray α) (f : α → m (Option β)) : m (Option β)
以相反的顺序将一元函数应用于子数组中的每个元素，并在函数成功的第一个元素处停止，返回 none 以外的值。返回后续值，如果不成功则返回 none。
例子：
#eval #["red", "green", "blue"].toSubarray.findSomeRevM? fun x => do
IO.println x
return Option.guard (· = 5) x.length
blue
greensome 5检查子数组中的所有元素是否满足布尔谓词。
从最低索引开始并向上移动元素进行测试。一旦找到不满足谓词的元素，搜索就会终止。
Subarray.allM.{u, w} {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Subarray α) : m BoolSubarray.allM.{u, w} {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Subarray α) : m Bool
检查子数组中的所有元素是否满足一元布尔谓词。
从最低索引开始并向上移动元素进行测试。一旦找到不满足谓词的元素，搜索就会终止。
例子：
#eval #["red", "green", "blue", "orange"].toSubarray.popFront.allM fun x => do
IO.println x
pure (x.length == 5)
green
bluefalse检查子数组中的任何元素是否满足布尔谓词。
从最低索引开始并向上移动元素进行测试。一旦找到满足谓词的元素，搜索就会终止。
Subarray.anyM.{u, w} {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Subarray α) : m BoolSubarray.anyM.{u, w} {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Subarray α) : m Bool
检查子数组中的任何元素是否满足一元布尔谓词。
从最低索引开始并向上移动元素进行测试。一旦找到满足谓词的元素，搜索就会终止。
例子：
#eval #["red", "green", "blue", "orange"].toSubarray.popFront.anyM fun x => do
IO.println x
pure (x == "blue")
green
bluetruetypedef struct {
lean_object m_header;
size_t m_size;
size_t m_capacity;
lean_object * m_data[];
} lean_array_object;
数组在 C 中的表示。更多细节请参阅运行时 Array 的说明。
bool lean_is_array(lean_object * o)
返回 true 表示 o 是数组；否则返回 false。
lean_array_object * lean_to_array(lean_object * o)
执行运行时检查，确认 o 确实是数组。如果 o 不是数组，断言将失败。