链接列表：有序列表，其中每个元素都有对下一个元素的引用。
链表上的大多数操作所花费的时间与链表的长度成正比，因为每个操作 必须遍历元素才能找到下一个元素。
List α 与 Array α 同构，但它们用于不同的事情：
构造子
List.nil.{u} {α : Type u} : List α
20.15. 链表
链表由 归纳类型 List 实现，包含一个有序的元素序列。
不同于 数组，Lean 会按照归纳类型的通常规则来编译列表；不过，借助 csimp 机制，某些列表操作在编译后的代码中会被替换为尾递归的等价实现。
Lean 同时为列表字面量和构造子 List.cons 提供了语法。
20.15.1. 语法
列表字面量写在方括号中，列表元素以逗号分隔。
把元素添加到列表头部的构造子 List.cons 用中缀运算符 «term_::_» : term:: 表示。
列表语法既可用于普通项，也可用于模式。
语法列表字面量
term ::= ...
|
The syntax [a, b, c] is shorthand for a :: b :: c :: [], or
List.cons a (List.cons b (List.cons c List.nil)). It allows conveniently constructing
list literals.
For lists of length at least 64, an alternative desugaring strategy is used
which uses let bindings as intermediates as in
let left := [d, e, f]; a :: b :: c :: left to avoid creating very deep expressions.
Note that this changes the order of evaluation, although it should not be observable
unless you use side effecting operations like dbg_trace.
Conventions for notations in identifiers:
-
The recommended spelling of
[]in identifiers isnil. -
The recommended spelling of
[a]in identifiers issingleton.
语法列表构造
term ::= ...
|
The list whose first element is head, where tail is the rest of the list.
Usually written head :: tail.
Conventions for notations in identifiers:
-
The recommended spelling of
::in identifiers iscons.
构造列表
模式匹配与列表
这些函数都彼此等价：
def split : List α → List α × List α
| [] => ([], [])
| [x] => ([x], [])
| x :: x' :: xs =>
let (ys, zs) := split xs
(x :: ys, x' :: zs)
def split' : List α → List α × List α
| .nil => (.nil, .nil)
| x :: [] => (.singleton x, .nil)
| x :: x' :: xs =>
let (ys, zs) := split xs
(x :: ys, x' :: zs)
def split'' : List α → List α × List α
| .nil => (.nil, .nil)
| .cons x .nil => (.singleton x, .nil)
| .cons x (.cons x' xs) =>
let (ys, zs) := split xs
(.cons x ys, .cons x' zs)
20.15.2. 性能说明
编译器不会覆盖或修改列表的表示：它们就是链表，每个元素都要经过一次指针间接访问。
计算列表长度需要完整遍历一次列表，而修改列表中的某个元素则需要遍历并重新分配该元素之前的前缀部分。
由于 Lean 使用基于引用计数的内存管理，像 List.map 这样遍历列表、并为原列表中的每个元素分配一个新的 List.cons 构造子的操作，在没有其他引用指向原列表时，可以复用原列表的内存。
由于列表在规约与说明中扮演着重要角色，大多数列表函数都尽可能直接地用结构递归编写。 这使得按归纳法编写证明更容易，但也意味着这些操作会消耗与列表长度成比例的栈空间。 许多列表函数都存在与其非尾递归版本等价的尾递归版本，但在推理时更难使用。 在编译后的代码中，尾递归版本会自动替代非尾递归版本。
20.15.3. 接口参考
20.15.3.1. 谓词与关系
定义
第一个列表是第二个列表的前缀。
IsPrefix l₁ l₂ 写作 l₁ <+: l₂，表示存在一些 t : List α，使得 l₂ 具有 l₁ ++ t 的形式。
函数 List.isPrefixOf 是布尔值等价函数。
标识符中的符号约定：
-
标识符中
<+:的建议拼写为prefix（而不是isPrefix）。
语法列表前缀
term ::= ...
| The first list is a prefix of the second.
IsPrefix l₁ l₂, written l₁ <+: l₂, means that there exists some t : List α such that l₂ has
the form l₁ ++ t.
The function List.isPrefixOf is a Boolean equivalent.
Conventions for notations in identifiers:
-
The recommended spelling of
<+:in identifiers isprefix(notisPrefix).
定义
第一个列表是第二个列表的后缀。
IsSuffix l₁ l₂ 写作 l₁ <:+ l₂，表示存在一些 t : List α，使得 l₂ 具有 t ++ l₁ 的形式。
函数 List.isSuffixOf 是布尔值等价函数。
标识符中的符号约定：
-
标识符中
<:+的建议拼写为suffix（而不是isSuffix）。
语法列表后缀
term ::= ...
| The first list is a suffix of the second.
IsSuffix l₁ l₂, written l₁ <:+ l₂, means that there exists some t : List α such that l₂ has
the form t ++ l₁.
The function List.isSuffixOf is a Boolean equivalent.
Conventions for notations in identifiers:
-
The recommended spelling of
<:+in identifiers issuffix(notisSuffix).
定义
语法列表中缀
term ::= ...
|
The first list is a contiguous sub-list of the second list. Typically written with the <:+:
operator.
In other words, l₁ <:+: l₂ means that there exist lists s : List α and t : List α such that
l₂ has the form s ++ l₁ ++ t.
Conventions for notations in identifiers:
-
The recommended spelling of
<:+:in identifiers isinfix(notisInfix).
归纳谓词
语法子列表
term ::= ...
|
The first list is a non-contiguous sub-list of the second list. Typically written with the <+
operator.
In other words, l₁ <+ l₂ means that l₁ can be transformed into l₂ by repeatedly inserting new
elements.
只有在打开 List 命名空间时，此语法才可用。
归纳谓词
如果两个列表包含相同的元素，并且每个列表出现相同的次数但不一定以相同的顺序，则它们是彼此的排列。
通过展示如何通过重复交换相邻元素将一个列表转换为另一个列表，可以证明一个列表是另一个列表的排列。
List.isPerm 是该关系的布尔等价值。
构造子
List.Perm.cons.{u} {α : Type u} (x : α) {l₁ l₂ : List α} : l₁.Perm l₂ → (x :: l₁).Perm (x :: l₂)
若一个列表是另一个列表的排列，则在二者头部添加相同元素后所得的列表也互为排列：l₁ ~ l₂ → x::l₁ ~ x::l₂。
List.Perm.swap.{u} {α : Type u} (x y : α) (l : List α) : (y :: x :: l).Perm (x :: y :: l)
若两个列表除前两个元素互换外完全相同，则它们互为排列：x::y::l ~ y::x::l。
List.Perm.trans.{u} {α : Type u} {l₁ l₂ l₃ : List α} : l₁.Perm l₂ → l₂.Perm l₃ → l₁.Perm l₃
排列具有传递性：l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃。
语法列表置换
term ::= ...
| Two lists are permutations of each other if they contain the same elements, each occurring the same number of times but not necessarily in the same order.
One list can be proven to be a permutation of another by showing how to transform one into the other by repeatedly swapping adjacent elements.
List.isPerm is a Boolean equivalent of this relation.
只有在打开 List 命名空间时，此语法才可用。
归纳谓词
列表中的每个元素都通过 R 与列表中所有后续元素相关。
Pairwise R l 表示 l 中索引较早的所有元素与索引较晚的所有元素都与 R 相关。
例如，Pairwise (· ≠ ·) l 断言 l 没有重复项，Pairwise (· < ·) l 断言 l 已（严格）排序。
示例：
-
Pairwise (· < ·) [1, 2, 3] ↔ (1 < 2 ∧ 1 < 3) ∧ 2 < 3 -
Pairwise (· = ·) [1, 2, 3] = False -
Pairwise (· ≠ ·) [1, 2, 3] = True
构造子
List.Pairwise.nil.{u} {α : Type u} {R : α → α → Prop} : List.Pairwise R []
空列表的所有元素之间自然两两满足给定关系。
List.Pairwise.cons.{u} {α : Type u} {R : α → α → Prop} {a : α} {l : List α} : (∀ (a' : α), a' ∈ l → R a a') → List.Pairwise R l → List.Pairwise R (a :: l)
定义
该列表没有重复项：它最多包含每个元素一次。
它被定义为Pairwise (· ≠ ·)：每个元素都不等于所有其他元素。
归纳谓词
列表的字典顺序与元素的顺序有关。
as 按字典顺序小于 bs，如果
-
as为空且bs非空，或者 -
as和bs均非空，且as的头部小于bs的头部r，或 -
as和bs都是非空的，它们的头相等，并且as的尾部小于bs的尾部。
20.15.3.2. 构造列表
定义
构造一个单元素列表。
示例：
-
List.singleton 5 = [5]。 -
List.singleton "green" = ["green"]。 -
List.singleton [1, 2, 3] = [[1, 2, 3]]
定义
将一个元素添加到列表的末尾。
添加的元素是结果列表的最后一个元素。
示例：
-
List.concat ["red", "yellow"] "green" = ["red", "yellow", "green"] -
List.concat [1, 2, 3] 4 = [1, 2, 3, 4] -
List.concat [] () = [()]
定义
创建一个包含 n 的 a 副本的列表。
-
List.replicate 5 "five" = ["five", "five", "five", "five", "five"] -
List.replicate 0 "zero" = [] -
List.replicate 2 ' ' = [' ', ' ']
定义
创建一个包含 n 的 a 副本的列表。
这是 List.replicate 的尾递归版本。
-
List.replicateTR 5 "five" = ["five", "five", "five", "five", "five"] -
List.replicateTR 0 "zero" = [] -
List.replicateTR 2 ' ' = [' ', ' ']
定义
定义
附加两个列表。通常通过 ++ 运算符使用。
追加列表所需的时间与第一个列表的长度成正比：O(|xs|)。
示例：
-
[1, 2, 3] ++ [4, 5] = [1, 2, 3, 4, 5]。 -
[] ++ [4, 5] = [4, 5]。 -
[1, 2, 3] ++ [] = [1, 2, 3]。
定义
附加两个列表。通常通过 ++ 运算符使用。
追加列表所需的时间与第一个列表的长度成正比：O(|xs|)。
这是 List.append 的尾递归版本。
示例：
-
[1, 2, 3] ++ [4, 5] = [1, 2, 3, 4, 5]。 -
[] ++ [4, 5] = [4, 5]。 -
[1, 2, 3] ++ [] = [1, 2, 3]。
定义
返回从 0 到 n（不包括）的数字列表，按升序排列。
O(n)。
示例：
-
range 5 = [0, 1, 2, 3, 4] -
range 0 = [] -
range 2 = [0, 1]
定义
返回具有给定长度 len 的数字列表，从 start 开始并增加
每个元素处都有 step。
换句话说，List.range' start len step 是 [start, start+step, ..., start+(len-1)*step]。
示例：
-
List.range' 0 3 (step := 1) = [0, 1, 2] -
List.range' 0 3 (step := 2) = [0, 2, 4] -
List.range' 0 4 (step := 2) = [0, 2, 4, 6] -
List.range' 3 4 (step := 2) = [3, 5, 7, 9]
定义
返回具有给定长度 len 的数字列表，从 start 开始并增加
每个元素处都有 step。
换句话说，List.range'TR start len step 是 [start, start+step, ..., start+(len-1)*step]。
这是 List.range' 的尾递归版本。
示例：
-
List.range'TR 0 3 (step := 1) = [0, 1, 2] -
List.range'TR 0 3 (step := 2) = [0, 2, 4] -
List.range'TR 0 4 (step := 2) = [0, 2, 4, 6] -
List.range'TR 3 4 (step := 2) = [3, 5, 7, 9]
定义
按顺序列出 Fin n 的所有元素，从 0 开始。
示例：
-
List.finRange 0 = ([] : List (Fin 0)) -
List.finRange 2 = ([0, 1] : List (Fin 2))
20.15.3.3. 长度
定义
20.15.3.4. 头与尾
定义
返回非空列表的第一个元素。
定义
返回列表中的第一个元素。如果列表为空，则会触发 panic并返回 default。
更安全的替代方案包括：
-
List.head，需要证明列表非空， -
List.head?，返回Option，并且 -
List.headD，它在空列表上返回显式提供的后备值。
定义
定义
定义
定义
删除非空列表的第一个元素并返回尾部。如果参数为空，则返回 none。
替代方案包括 List.tail（失败时返回空列表）、List.tail?（返回 Option）和 List.tail!（在空列表上触发错误）。
示例：
20.15.3.5. 查找
定义
定义
定义
定义
定义
返回列表中的最后一个元素；如果列表为空，则返回 fallback。
替代方案包括 List.getLast?（返回 Option）和 List.getLast!（在空列表上触发 panic）。
示例：
定义
定义
定义
20.15.3.6. 查询
定义
定义
定义
定义
定义
定义
返回 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
定义
定义
定义
定义
定义
List.findSomeM?.{u, v, w} {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m (Option β)) : List α → m (Option β)List.findSomeM?.{u, v, w} {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m (Option β)) : List α → m (Option β)
返回将一元函数 none 应用于每个元素的第一个非 f 结果
列表，按顺序。如果 none 对所有元素返回 f，则返回 none。
O(|l|)。
示例：
#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 1020.15.3.7. 转换
定义
O(|xs|)。在运行时，该操作由 List.toArrayImpl 实现，并且花费的时间与
列表的长度。应使用 List.toArray 代替 Array.mk。
示例：
-
[1, 2, 3].toArray = #[1, 2, 3] -
["monday", "wednesday", friday"].toArray = #["monday", "wednesday", friday"].
定义
通过重复将列表中的元素推入空列表，将 List α 转换为 Array α
数组。 O(|xs|)。
使用 List.toArray 而不是直接调用该函数。在运行时，该操作实现
List.toArray 和 Array.mk。
定义
将浮点数列表转换为 FloatArray。
定义
20.15.3.8. 修改
定义
定义
定义
定义
将列表的头部替换为应用 f 的结果。如果列表为空，则返回空列表。
示例：
-
[1, 2, 3].modifyHead (· * 10) = [10, 2, 3] -
[].modifyHead (· * 10) = []
定义
将第 n 个 l 的尾部替换为对其应用 f 的结果。如果索引大于列表的长度，则返回输入而不使用 f。
示例：
["circle", "square", "triangle"].modifyTailIdx 1 List.reverse["circle", "triangle", "square"]["circle", "square", "triangle"].modifyTailIdx 1 (fun xs => xs ++ xs)["circle", "square", "triangle", "square", "triangle"]["circle", "square", "triangle"].modifyTailIdx 2 (fun xs => xs ++ xs)["circle", "square", "triangle", "triangle"]["circle", "square", "triangle"].modifyTailIdx 5 (fun xs => xs ++ xs)["circle", "square", "triangle"]
定义
定义
定义
定义
删除指定索引处的元素。如果索引越界，则列表将不加修改地返回。
O(i)。
这是 List.eraseIdx 的尾递归版本，在运行时使用。
示例：
-
[0, 1, 2, 3, 4].eraseIdxTR 0 = [1, 2, 3, 4] -
[0, 1, 2, 3, 4].eraseIdxTR 1 = [0, 2, 3, 4] -
[0, 1, 2, 3, 4].eraseIdxTR 5 = [0, 1, 2, 3, 4]
定义
定义
定义
定义
返回 l 从索引 start（包含）到 stop（不包含）的切片。
示例：
-
[0, 1, 2, 3, 4, 5].extract 1 2 = [1]
-
[0, 1, 2, 3, 4, 5].extract 2 2 = []
-
[0, 1, 2, 3, 4, 5].extract 2 4 = [2, 3]
-
[0, 1, 2, 3, 4, 5].extract 2 = [2, 3, 4, 5]
-
[0, 1, 2, 3, 4, 5].extract (stop := 2) = [0, 1]
定义
定义
定义
定义
定义
将 xs 的元素向左旋转，将 i % xs.length 元素从列表的开头移动到结尾。
O(|xs|)。
示例：
-
[1, 2, 3, 4, 5].rotateLeft 3 = [4, 5, 1, 2, 3] -
[1, 2, 3, 4, 5].rotateLeft 5 = [1, 2, 3, 4, 5] -
[1, 2, 3, 4, 5].rotateLeft 1 = [2, 3, 4, 5, 1]
定义
将 xs 的元素向右旋转，将 i % xs.length 元素从列表末尾移动到开头。
旋转后，xs[n] 处的元素位于索引 (i + n) % l.length 处。 O(|xs|)。
示例：
-
[1, 2, 3, 4, 5].rotateRight 3 = [3, 4, 5, 1, 2] -
[1, 2, 3, 4, 5].rotateRight 5 = [1, 2, 3, 4, 5] -
[1, 2, 3, 4, 5].rotateRight 1 = [5, 1, 2, 3, 4]
定义
在左侧填充 l : List α，并重复出现 a : α，直到其长度为 n。如果 l 已至少具有 n 元素，则返回未修改的元素。
这是 List.leftpad 的尾递归版本，在运行时使用。
示例：
-
[1, 2, 3].leftPadTR 5 0 = [0, 0, 1, 2, 3] -
["red", "green", "blue"].leftPadTR 4 "blank" = ["blank", "red", "green", "blue"] -
["red", "green", "blue"].leftPadTR 3 "blank" = ["red", "green", "blue"] -
["red", "green", "blue"].leftPadTR 1 "blank" = ["red", "green", "blue"]
20.15.3.8.1. 插入
定义
定义
将元素插入列表中指定索引处。如果索引大于列表的长度，则列表将不加修改地返回。
换句话说，新元素被插入到列表 l 中前 i 个元素之后；此列表即 l。
示例：
定义
将元素插入列表中指定索引处。如果索引大于列表的长度，则列表将不加修改地返回。
换句话说，新元素被插入到列表 l 中前 i 个元素之后；此列表即 l。
这是 List.insertIdx 的尾递归版本，在运行时使用。
示例：
-
["tues", "thur", "sat"].insertIdxTR 1 "wed" = ["tues", "wed", "thur", "sat"] -
["tues", "thur", "sat"].insertIdxTR 2 "wed" = ["tues", "thur", "wed", "sat"] -
["tues", "thur", "sat"].insertIdxTR 3 "wed" = ["tues", "thur", "sat", "wed"] -
["tues", "thur", "sat"].insertIdxTR 4 "wed" = ["tues", "thur", "sat"]
定义
将 l 与 sep 的元素交替。
O(|l|)。
List.intercalate 是一个类似的函数，它将分隔符列表与列表列表的元素交替。
示例：
-
List.intersperse "then" [] = [] -
List.intersperse "then" ["walk"] = ["walk"] -
List.intersperse "then" ["walk", "run"] = ["walk", "then", "run"] -
List.intersperse "then" ["walk", "run", "rest"] = ["walk", "then", "run", "then", "rest"]
定义
将 l 与 sep 的元素交替。
O(|l|)。
这是 List.intersperse 的尾递归版本，在运行时使用。
示例：
-
List.intersperseTR "then" [] = [] -
List.intersperseTR "then" ["walk"] = ["walk"] -
List.intersperseTR "then" ["walk", "run"] = ["walk", "then", "run"] -
List.intersperseTR "then" ["walk", "run", "rest"] = ["walk", "then", "run", "then", "rest"]
定义
将 xs 中的列表与分隔符 sep 交替，并附加它们。结果列表被展平。
O(|xs|)。
List.intersperse 是一个类似的函数，它将分隔符元素与列表的元素交替。
示例：
-
List.intercalate sep [] = [] -
List.intercalate sep [a] = a -
List.intercalate sep [a, b] = a ++ sep ++ b -
List.intercalate sep [a, b, c] = a ++ sep ++ b ++ sep ++ c
定义
将 xs 中的列表与分隔符 sep 交替。
这是运行时使用的 List.intercalate 的尾递归版本。
示例：
-
List.intercalateTR sep [] = [] -
List.intercalateTR sep [a] = a -
List.intercalateTR sep [a, b] = a ++ sep ++ b -
List.intercalateTR sep [a, b, c] = a ++ sep ++ b ++ sep ++ c
20.15.3.9. 排序
定义
List.mergeSort.{u_1} {α : Type u_1} (xs : List α) (le : α → α → Bool := by exact fun a b => a ≤ b) : List αList.mergeSort.{u_1} {α : Type u_1} (xs : List α) (le : α → α → Bool := by exact fun a b => a ≤ b) : List α
定义
List.merge.{u_1} {α : Type u_1} (xs ys : List α) (le : α → α → Bool := by exact fun a b => a ≤ b) : List αList.merge.{u_1} {α : Type u_1} (xs ys : List α) (le : α → α → Bool := by exact fun a b => a ≤ b) : List α
合并两个列表，如果两者都是，则使用 le 选择结果列表的第一个元素
非空。
如果两个输入列表都根据 le 排序，则结果列表也根据
至 le。 O(|xs| + |ys|)。
此实现不是尾递归的，但它在运行时被经过验证的等效实现替换 尾递归合并。
20.15.3.10. 迭代
定义
定义
定义
List.forA.{u, v, w} {m : Type u → Type v} [Applicative m] {α : Type w} (as : List α) (f : α → m PUnit) : m PUnitList.forA.{u, v, w} {m : Type u → Type v} [Applicative m] {α : Type w} (as : List α) (f : α → m PUnit) : m PUnit
定义
List.forM.{u, v, w} {m : Type u → Type v} [Monad m] {α : Type w} (as : List α) (f : α → m PUnit) : m PUnitList.forM.{u, v, w} {m : Type u → Type v} [Monad m] {α : Type w} (as : List α) (f : α → m PUnit) : m PUnit
按顺序将一元操作 f 应用于列表中的每个元素。
List.mapM 是一个收集结果的变体。 List.forA 是一个适用于任何
Applicative。
定义
List.firstM.{u, v, w} {m : Type u → Type v} [Alternative m] {α : Type w} {β : Type u} (f : α → m β) : List α → m βList.firstM.{u, v, w} {m : Type u → Type v} [Alternative m] {α : Type w} {β : Type u} (f : α → m β) : List α → m β
将 f 映射到列表并使用 <|> 收集结果。列表末尾的结果是
failure。
示例：
-
[[], [1, 2], [], [2]].firstM List.head? = some 1 -
[[], [], []].firstM List.head? = none -
[].firstM List.head? = none
定义
20.15.3.10.1. 折叠
折叠是使用某个函数将列表元素组合起来的运算。 根据函数调用的嵌套方式，它们分为两类：
- 左折叠
左折叠从列表头开始向末尾依次组合元素。 列表头会先与初始值组合，该结果再与下一个值组合，依此类推。
- 右折叠
右折叠从列表尾开始向开头组合元素，就像把每个
cons构造子替换成一次对组合函数的调用，并把nil替换成初始值一样。
带 -M 后缀的单子折叠允许组合函数使用某个 单子 中的效应，这也可能包括提前终止折叠。
定义
定义
List.foldlM.{u, v, w} {m : Type u → Type v} [Monad m] {s : Type u} {α : Type w} (f : s → α → m s) (init : s) : List α → m sList.foldlM.{u, v, w} {m : Type u → Type v} [Monad m] {s : Type u} {α : Type w} (f : s → α → m s) (init : s) : List α → m s
将一元函数从左侧折叠到列表上，累积以 init 开头的值。的
累积值使用 f 按顺序与列表中的每个元素组合。
示例：
example [Monad m] (f : α → β → m α) :
List.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
定义
List.foldlRecOn.{u_1, u_2, u_3} {β : Type u_1} {α : Type u_2} {motive : β → Sort u_3} (l : List α) (op : β → α → β) {b : β} : motive b → ((b : β) → motive b → (a : α) → a ∈ l → motive (op b a)) → motive (List.foldl op b l)List.foldlRecOn.{u_1, u_2, u_3} {β : Type u_1} {α : Type u_2} {motive : β → Sort u_3} (l : List α) (op : β → α → β) {b : β} : motive b → ((b : β) → motive b → (a : α) → a ∈ l → motive (op b a)) → motive (List.foldl op b l)
通过建立对初始数据成立且被折叠操作保持的不变量，证明有关 List.foldl 结果的命题。
此段说明该操作的行为、边界条件及推荐用法。
示例：
example {xs : List Nat} : xs.foldl (· + ·) 1 > 0 := xs:List Nat⊢ List.foldl (fun x1 x2 => x1 + x2) 1 xs > 0
xs:List Nat⊢ 0 < 1xs:List Nat⊢ ∀ (b : Nat), 0 < b → ∀ (a : Nat), a ∈ xs → 0 < b + a
xs:List Nat⊢ 0 < 1 xs:List Nat⊢ 0 < 1; All goals completed! 🐙
xs:List Nat⊢ ∀ (b : Nat), 0 < b → ∀ (a : Nat), a ∈ xs → 0 < b + a xs:List Nat⊢ ∀ (b : Nat), 0 < b → ∀ (a : Nat), a ∈ xs → 0 < b + a
xs:List Natb✝:Nata✝²:0 < b✝a✝¹:Nata✝:a✝¹ ∈ xs⊢ 0 < b✝ + a✝¹; All goals completed! 🐙
定义
定义
List.foldrM.{u, v, w} {m : Type u → Type v} [Monad m] {s : Type u} {α : Type w} (f : α → s → m s) (init : s) (l : List α) : m sList.foldrM.{u, v, w} {m : Type u → Type v} [Monad m] {s : Type u} {α : Type w} (f : α → s → m s) (init : s) (l : List α) : m s
从右侧用单子函数折叠列表，以 init 为初值，并用 f 按逆序把每个元素与累积值结合。
示例：
example [Monad m] (f : α → β → m β) :
List.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
定义
List.foldrRecOn.{u_1, u_2, u_3} {β : Type u_1} {α : Type u_2} {motive : β → Sort u_3} (l : List α) (op : α → β → β) {b : β} : motive b → ((b : β) → motive b → (a : α) → a ∈ l → motive (op a b)) → motive (List.foldr op b l)List.foldrRecOn.{u_1, u_2, u_3} {β : Type u_1} {α : Type u_2} {motive : β → Sort u_3} (l : List α) (op : α → β → β) {b : β} : motive b → ((b : β) → motive b → (a : α) → a ∈ l → motive (op a b)) → motive (List.foldr op b l)
通过建立对初始数据成立且被折叠操作保持的不变量，证明有关 List.foldr 结果的命题。
此段说明该操作的行为、边界条件及推荐用法。
示例：
example {xs : List Nat} : xs.foldr (· + ·) 1 > 0 := xs:List Nat⊢ List.foldr (fun x1 x2 => x1 + x2) 1 xs > 0
xs:List Nat⊢ 0 < 1xs:List Nat⊢ ∀ (b : Nat), 0 < b → ∀ (a : Nat), a ∈ xs → 0 < a + b
xs:List Nat⊢ 0 < 1 xs:List Nat⊢ 0 < 1; All goals completed! 🐙
xs:List Nat⊢ ∀ (b : Nat), 0 < b → ∀ (a : Nat), a ∈ xs → 0 < a + b xs:List Nat⊢ ∀ (b : Nat), 0 < b → ∀ (a : Nat), a ∈ xs → 0 < a + b
xs:List Natb✝:Nata✝²:0 < b✝a✝¹:Nata✝:a✝¹ ∈ xs⊢ 0 < a✝¹ + b✝; All goals completed! 🐙
定义
从右侧折叠列表，以 init 为初值，并用 f 按逆序把每个元素与累积值结合。
这是相应函数的尾递归版本，并在运行时代码中使用。（相关项：O(|l|)、List.foldr。）
以下列出相应示例或例外情况。
20.15.3.11. 转换
定义
定义
定义
List.mapM.{u, v, w} {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m β) (as : List α) : m (List β)List.mapM.{u, v, w} {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m β) (as : List α) : m (List β)
将单子操作 f 从左到右应用于列表中的每个元素，并返回结果列表。
这个实现是尾递归的。 List.mapM' 是一种非尾递归变体，可能更方便推理。 List.forM 是丢弃结果的变体，List.mapA 是与 Applicative 一起使用的变体。
定义
List.mapM'.{u_1, u_2, u_3} {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → m β) : List α → m (List β)List.mapM'.{u_1, u_2, u_3} {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → m β) : List α → m (List β)
从左到右对列表中的每个元素应用一元操作 f，并返回结果列表。
这是 List.mapM 的非尾递归变体，更容易推理。它不能用作主定义并被尾递归版本替换，因为只有当 m 是 LawfulMonad 时才能证明它们相等。
定义
List.mapA.{u, v, w} {m : Type u → Type v} [Applicative m] {α : Type w} {β : Type u} (f : α → m β) : List α → m (List β)List.mapA.{u, v, w} {m : Type u → Type v} [Applicative m] {α : Type w} {β : Type u} (f : α → m β) : List α → m (List β)
定义
将函数应用于列表中的每个元素以及找到该元素的索引，返回结果列表。除了索引之外，该函数还提供了索引有效的证明。
List.mapIdx 是一个变体，它不向函数提供索引有效的证据。
定义
将一元函数应用于列表中的每个元素以及找到该元素的索引，返回结果列表。除了索引之外，该函数还提供了索引有效的证明。
List.mapIdxM 是一个变体，它不向函数提供索引有效的证据。
定义
List.mapIdxM.{u_1, u_2, u_3} {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : Nat → α → m β) (as : List α) : m (List β)List.mapIdxM.{u_1, u_2, u_3} {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : Nat → α → m β) (as : List α) : m (List β)
将一元函数应用于列表的每个元素以及找到该元素的索引，返回结果列表。
List.mapFinIdxM 是一个变体，它另外为该函数提供索引有效的证明。
定义
将函数应用于列表的每个元素，返回结果列表。该函数是单态的：要求返回相同类型的值。内部实现使用指针相等，并且如果每个函数调用的结果与其参数指针相等，则不会分配新列表。
出于验证目的，List.mapMono = List.map。
定义
List.mapMonoM.{u_1, u_2} {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] (as : List α) (f : α → m α) : m (List α)List.mapMonoM.{u_1, u_2} {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] (as : List α) (f : α → m α) : m (List α)
将一元函数应用于列表的每个元素，返回结果列表。该函数是单态的：要求返回相同类型的值。内部实现使用指针相等，并且如果每个函数调用的结果与其参数指针相等，则不会分配新列表。
定义
应用一个函数，将列表返回到列表的每个元素，并连接结果列表。
示例：
-
[2, 3, 2].flatMap List.range = [0, 1, 0, 1, 2, 0, 1] -
["red", "blue"].flatMap String.toList = ['r', 'e', 'd', 'b', 'l', 'u', 'e']
定义
应用一个函数，将列表返回到列表的每个元素，并连接结果列表。
这是运行时使用的 List.flatMap 的尾递归版本。
示例：
-
[2, 3, 2].flatMapTR List.range = [0, 1, 0, 1, 2, 0, 1] -
["red", "blue"].flatMapTR String.toList = ['r', 'e', 'd', 'b', 'l', 'u', 'e']
定义
List.flatMapM.{u, v, w} {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m (List β)) (as : List α) : m (List β)List.flatMapM.{u, v, w} {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m (List β)) (as : List α) : m (List β)
应用一个单子函数，该函数从左到右将列表返回到列表中的每个元素，并连接结果列表。
定义
定义
定义
List.zipWith.{u, v, w} {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (xs : List α) (ys : List β) : List γList.zipWith.{u, v, w} {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (xs : List α) (ys : List β) : List γ
定义
List.zipWithTR.{u_1, u_2, u_3} {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (as : List α) (bs : List β) : List γList.zipWithTR.{u_1, u_2, u_3} {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (as : List α) (bs : List β) : List γ
定义
定义
定义
20.15.3.12. 过滤
定义
定义
List.filterM.{v} {m : Type → Type v} [Monad m] {α : Type} (p : α → m Bool) (as : List α) : m (List α)List.filterM.{v} {m : Type → Type v} [Monad m] {α : Type} (p : α → m Bool) (as : List α) : m (List α)
从左到右依次把单子谓词 p 应用于列表中的每个元素，并返回使 p 返回 true 的元素。
O(|l|).
示例：
#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]
定义
List.filterRevM.{v} {m : Type → Type v} [Monad m] {α : Type} (p : α → m Bool) (as : List α) : m (List α)List.filterRevM.{v} {m : Type → Type v} [Monad m] {α : Type} (p : α → m Bool) (as : List α) : m (List α)
从右到左逆序把单子谓词 p 应用于列表中的每个元素，并返回使 p 返回 true 的元素；结果仍保持输入顺序。
示例：
#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 值。
这是相应函数的尾递归版本，并在运行时代码中使用。（相关项：O(|l|)、List.filterMap。）
示例：
#eval [1, 2, 5, 2, 7, 7].filterMapTR fun x =>
if x > 2 then some (2 * x) else none
[10, 14, 14]
定义
List.filterMapM.{u, v, w} {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m (Option β)) (as : List α) : m (List β)List.filterMapM.{u, v, w} {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m (Option β)) (as : List α) : m (List β)
把返回 Option 的单子函数应用于列表的每个元素，并收集所有非 none 值。
O(|l|).
示例：
#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]20.15.3.12.1. 分割
定义
定义
定义
定义
返回 xs 中 p 返回 true 的最长初始段。
O(|xs|)。这是 List.take 的尾递归版本，在运行时使用。
示例：
-
[7, 6, 4, 8].takeWhileTR (· > 5) = [7, 6] -
[7, 6, 6, 5].takeWhileTR (· > 5) = [7, 6, 6] -
[7, 6, 6, 8].takeWhileTR (· > 5) = [7, 6, 6, 8]
定义
定义
定义
定义
删除列表的最后一个元素（如果存在）。
这是 List.dropLast 的尾递归版本，在运行时使用。
示例：
-
[].dropLastTR = [] -
["tea"].dropLastTR = [] -
["tea", "coffee", "juice"].dropLastTR = ["tea", "coffee"]
定义
在索引处拆分列表，结果将前 n 个 l 的元素与剩余元素配对。
如果 n 大于 l 的长度，则结果对由 l 和空列表组成。List.splitAt 等价于组合使用 List.take 和 List.drop，但效率更高。
示例：
-
["red", "green", "blue"].splitAt 2 = (["red", "green"], ["blue"]) -
["red", "green", "blue"].splitAt 3 = (["red", "green", "blue], []) -
["red", "green", "blue"].splitAt 4 = (["red", "green", "blue], [])
定义
定义
将列表拆分为最长的段，其中每对相邻元素通过 R 相关。
O(|l|)。
示例：
定义
定义
返回一对列表，它们一起包含 as 的所有元素。第一个列表包含单子谓词 p 返回 true 的元素，第二个列表包含 p 返回 false 的元素。按从左到右的顺序检查列表的元素。
这是 List.partition 的一元版本。
例子：
def posOrNeg (x : Int) : Except String Bool :=
if x > 0 then pure true
else if x < 0 then pure false
else throw "Zero is not positive or negative"
#eval [-1, 2, 3].partitionM posOrNeg
Except.ok ([2, 3], [-1])#eval [0, 2, 3].partitionM posOrNeg
Except.error "Zero is not positive or negative"
定义
定义
List.groupByKey.{u, v} {α : Type u} {β : Type v} [BEq α] [Hashable α] (key : β → α) (xs : List β) : Std.HashMap α (List β)List.groupByKey.{u, v} {α : Type u} {β : Type v} [BEq α] [Hashable α] (key : β → α) (xs : List β) : Std.HashMap α (List β)
根据列表 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])]20.15.3.13. 元素判定
定义
定义
定义
定义
定义
定义
定义
定义
20.15.3.14. 比较
定义
定义
返回 true，如果 l₁ 和 l₂ 互为排列。复杂度为 O(|l₁| * |l₂|)。
关系 List.Perm 是排列的逻辑刻画。当 BEq α 实例与 DecidableEq α 对应时，isPerm l₁ l₂ ↔ l₁ ~ l₂（使用定理 isPerm_iff）。
定义
检查第一个列表是否为第二个列表的前缀。
关系 List.IsPrefixOf 使用逻辑相等来表达此性质。
示例：
-
[1, 2].isPrefixOf [1, 2, 3] = true -
[1, 2].isPrefixOf [1, 2] = true -
[1, 2].isPrefixOf [1] = false -
[1, 2].isPrefixOf [1, 1, 2, 3] = false
定义
如果第一个列表是第二个列表的前缀，则返回从第二个列表中去掉该前缀后的结果。
换言之，isPrefixOf? l₁ l₂ 返回 some t，当且仅当 l₂ == l₁ ++ t。
示例：
-
[1, 2].isPrefixOf? [1, 2, 3] = some [3] -
[1, 2].isPrefixOf? [1, 2] = some [] -
[1, 2].isPrefixOf? [1] = none -
[1, 2].isPrefixOf? [1, 1, 2, 3] = none
定义
检查第一个列表是否为第二个列表的后缀。
关系 List.IsSuffixOf 使用逻辑相等来表达此性质。
示例：
-
[2, 3].isSuffixOf [1, 2, 3] = true -
[2, 3].isSuffixOf [1, 2, 3, 4] = false -
[2, 3].isSuffixOf [1, 2] = false -
[2, 3].isSuffixOf [1, 1, 2, 3] = true
定义
如果第一个列表是第二个列表的后缀，则返回从第二个列表中去掉该后缀后的结果。
换言之，isSuffixOf? l₁ l₂ 返回 some t，当且仅当 l₂ == t ++ l₁。
示例：
-
[2, 3].isSuffixOf? [1, 2, 3] = some [1] -
[2, 3].isSuffixOf? [1, 2, 3, 4] = none -
[2, 3].isSuffixOf? [1, 2] = none -
[2, 3].isSuffixOf? [1, 1, 2, 3] = some [1, 1]
定义
列表相对于其元素严格顺序的非严格顺序。
as ≤ bs 成立，如果 ¬ bs < as。
如果底层 LT α 实例具有良好性质，则可将此关系视为字典序。具体而言，它应满足非自反性、非对称性和反对称性。这些要求在 List.cons_le_cons_iff 中有精确表述。若这些性质成立，则 as ≤ bs 当且仅当：
-
as为空；或 -
as和bs都非空，且as的首元素小于bs的首元素；或 -
as和bs都非空、首元素相等，且as的尾部小于或等于bs的尾部。
定义
列表相对于其元素顺序的字典序。
当满足以下条件之一时，as < bs：
-
as为空且bs非空；或 -
as和bs都非空，且as的首元素小于bs的首元素；或 -
as和bs都非空、首元素相等，且as的尾部小于bs的尾部。
定义
20.15.3.15. 终止辅助
定义
定义
为满足谓词 P 的值列表逐一“附加”证明，返回相应子类型 { x // P x } 中的元素列表。
O(1).
定义
忘掉子类型元素满足谓词的证明，把子类型中的项列表映射回原类型中的相应项。
它与所列操作对应或等价。（相关项：List.attachWith、l.map (·.val)。）
此段说明该操作的行为、边界条件及推荐用法。（相关项：map_subtype、unattach_attach。）
此函数主要用于良基递归的终止性证明，使迭代操作取得的值能与原参数建立所需关系。（相关项：相关说明、simp [List.unattach, -List.map_subtype]。）
定义
List.pmap.{u_1, u_2} {α : Type u_1} {β : Type u_2} {P : α → Prop} (f : (a : α) → P a → β) (l : List α) (H : ∀ (a : α), a ∈ l → P a) : List βList.pmap.{u_1, u_2} {α : Type u_1} {β : Type u_2} {P : α → Prop} (f : (a : α) → P a → β) (l : List α) (H : ∀ (a : α), a ∈ l → P a) : List β