Lean 的标准库包含一个规范的链表数据类型，称为 List，并提供了使其使用更方便的特殊语法。 列表写在方括号中。 例如，一个包含小于 10 的素数的列表可以写作：

def primesUnder10 : List Nat := [2, 3, 5, 7]

在幕后，List 是一个归纳数据类型，其定义如下：

inductive List (α : Type) where | nil : List α | cons : α → List α → List α

标准库中的实际定义略有不同，因为它使用了尚未介绍的特性，但二者在实质上是相似的。 这个定义说明，List 与 PPoint 一样，以单个类型作为其参数。 这个类型就是列表中所存储条目的类型。 根据这些构造子，可以用 nil 或 cons 构造一个 List α。 构造子 nil 表示空列表，而构造子 cons 用于非空列表。 cons 的第一个参数是列表的头部，第二个参数是其尾部。 一个包含 n 个条目的列表包含 n 个 cons 构造子，其中最后一个以 nil 作为其尾部。

primesUnder10 示例可以通过直接使用 List 的构造子写得更显式：

def explicitPrimesUnder10 : List Nat := List.cons 2 (List.cons 3 (List.cons 5 (List.cons 7 List.nil)))

这两个定义完全等价，但 primesUnder10 比 explicitPrimesUnder10 容易读得多。

消费 List 的函数可以用与消费 Nat 的函数大致相同的方式来定义。 事实上，理解链表的一种方式是把它看作一个 Nat，其中每个 succ 构造子上都悬挂着一个额外的数据字段。 从这个角度看，计算列表长度的过程就是把每个 cons 替换为一个 succ，并把最后的 nil 替换为一个 zero。 正如 replaceX 以点的字段类型作为参数一样，length 以列表条目的类型作为参数。 例如，如果列表包含字符串，那么第一个参数就是 String：length String ["Sourdough", "bread"]。 它应当像这样计算：

length 的定义既是多态的（因为它将列表元素类型作为实参），也是递归的（因为它引用自身）。 一般而言，函数遵循数据的形状：递归数据类型导向递归函数，多态数据类型导向多态函数。

def length (α : Type) (xs : List α) : Nat := match xs with | List.nil => Nat.zero | List.cons y ys => Nat.succ (length α ys)

为了使列表上的函数更易读，可以使用方括号记法 [] 来对 nil 进行模式匹配，并且可以用中缀 :: 来代替 cons：

def length (α : Type) (xs : List α) : Nat := match xs with | [] => 0 | y :: ys => Nat.succ (length α ys)

replaceX 和 length 使用起来都有些繁琐，因为类型参数通常由后面的值唯一确定。 事实上，在大多数语言中，编译器完全能够自行确定类型参数，只是偶尔需要用户提供帮助。 在 Lean 中也是如此。 定义函数时，可以通过用花括号而非圆括号包住参数来将参数声明为隐式。 例如，带有隐式类型参数的 replaceX 版本如下所示：

def replaceX {α : Type} (point : PPoint α) (newX : α) : PPoint α := { point with x := newX }

它可以与 natOrigin 一起使用，而无需显式提供 Nat，因为 Lean 可以从后续参数中推断出 α 的值：

{ x := 5, y := 0 }#eval replaceX natOrigin 5

{ x := 5, y := 0 }

类似地，length 可以重新定义为隐式地接受元素类型：

def length {α : Type} (xs : List α) : Nat := match xs with | [] => 0 | y :: ys => Nat.succ (length ys)

这个 length 函数可以直接应用于 primesUnder10：

4#eval length primesUnder10

4

在标准库中，Lean 将这个函数称为 List.length，这意味着用于访问结构字段的点语法也可以用来求列表的长度：

4#eval primesUnder10.length

4

正如 C# 和 Java 有时要求显式提供类型实参一样，Lean 并不总是能够找到隐式参数。 在这些情况下，可以使用它们的名称来提供它们。 例如，可以通过将 α 设为 Int，来指定一个只适用于整数列表的 List.length 版本：

List.length : List Int → Nat#check List.length (α := Int)

List.length : List Int → Nat

并非所有可定义的结构或归纳类型都能具有类型 Type。 特别地，如果某个构造子以任意类型作为参数，那么该归纳类型必须具有不同的类型。 这些错误通常会说明一些关于“宇宙层级”的内容。 例如，对于这个归纳类型：

inductive MyType : Type where Invalid universe level in constructor `MyType.ctor`: Parameter `α` has type Type at universe level 2 which is not less than or equal to the inductive type's resulting universe level 1| ctor : (α : Type) → α → MyType

Lean 给出如下错误：

Invalid universe level in constructor `MyType.ctor`: Parameter `α` has type
  Type
at universe level
  2
which is not less than or equal to the inductive type's resulting universe level
  1

后面的章节会说明为什么会这样，以及如何修改定义以使其工作。 目前，请尝试把该类型作为整个归纳类型的参数，而不是作为构造子的参数。

类似地，如果某个构造子的实参是一个以正在定义的数据类型作为实参的函数，那么该定义会被拒绝。 例如：

(kernel) arg #1 of 'MyType.ctor' has a non positive occurrence of the datatypes being declaredinductive MyType : Type where | ctor : (MyType → Int) → MyType

会产生消息：

(kernel) arg #1 of 'MyType.ctor' has a non positive occurrence of the datatypes being declared

出于技术原因，允许这些数据类型可能会使 Lean 的内部逻辑受到破坏，从而使其不适合用作定理证明器。

接受两个参数的递归函数不应对参数对进行匹配，而应分别独立地匹配每个参数。 否则，Lean 中用于检查递归调用是否作用于更小值的机制，无法看出输入值与递归调用中的实参之间的联系。 例如，下面这个判断两个列表是否具有相同长度的函数会被拒绝：

def fail to show termination for sameLength with errors failed to infer structural recursion: Not considering parameter α of sameLength: it is unchanged in the recursive calls Not considering parameter β of sameLength: it is unchanged in the recursive calls Cannot use parameter xs: failed to eliminate recursive application sameLength xs' ys' Cannot use parameter ys: failed to eliminate recursive application sameLength xs' ys' Could not find a decreasing measure. The basic measures relate at each recursive call as follows: (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted) xs ys 1) 1816:28-46 ? ? Please use `termination_by` to specify a decreasing measure.sameLength (xs : List α) (ys : List β) : Bool := match (xs, ys) with | ([], []) => true | (x :: xs', y :: ys') => sameLength xs' ys' | _ => false

错误消息为：

fail to show termination for
  sameLength
with errors
failed to infer structural recursion:
Not considering parameter α of sameLength:
  it is unchanged in the recursive calls
Not considering parameter β of sameLength:
  it is unchanged in the recursive calls
Cannot use parameter xs:
  failed to eliminate recursive application
    sameLength xs' ys'
Cannot use parameter ys:
  failed to eliminate recursive application
    sameLength xs' ys'


Could not find a decreasing measure.
The basic measures relate at each recursive call as follows:
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
              xs ys
1) 1816:28-46  ?  ?
Please use `termination_by` to specify a decreasing measure.

这个问题可以通过嵌套模式匹配来修正：

def sameLength (xs : List α) (ys : List β) : Bool := match xs with | [] => match ys with | [] => true | _ => false | x :: xs' => match ys with | y :: ys' => sameLength xs' ys' | _ => false

同时匹配 将在下一节介绍，它是解决该问题的另一种方式，而且通常更为优雅。

忘记给归纳类型传递参数也可能产生令人困惑的消息。 例如，当在 ctor 的类型中没有将参数 α 传递给 MyType 时：

inductive MyType (α : Type) : Type where | ctor : α → type expected, got (MyType : Type → Type)MyType

Lean 给出如下错误：

type expected, got
  (MyType : Type → Type)

错误消息是在说明，MyType 的类型，即 Type → Type，其本身并不描述类型。 MyType 需要一个参数才能成为一个真正的类型。

当在其他上下文中省略类型参数时，也可能出现同样的消息，例如在某个定义的类型签名中：

inductive MyType (α : Type) : Type where | ctor : α → MyType αdef ofFive : type expected, got (MyType : Type → Type)MyType := ctor 5

type expected, got
  (MyType : Type → Type)

对使用多态类型的表达式求值时，可能会触发 Lean 无法显示某个值的情形。 #eval 命令会对所提供的表达式求值，并使用该表达式的类型来确定如何显示结果。 对于某些类型（例如函数），这一过程会失败，但对于大多数其他类型，Lean 完全能够自动生成显示代码。 例如，不需要为 WoodSplittingTool 向 Lean 提供任何特定的显示代码：

inductive WoodSplittingTool where | axe | maul | froeWoodSplittingTool.axe#eval WoodSplittingTool.axe

WoodSplittingTool.axe

不过，Lean 在这里使用的自动化是有限度的。 allTools 是包含全部三个工具的列表：

def allTools : List WoodSplittingTool := [ WoodSplittingTool.axe, WoodSplittingTool.maul, WoodSplittingTool.froe ]

对它求值会导致错误：

could not synthesize a `ToExpr`, `Repr`, or `ToString` instance for type List WoodSplittingTool#eval allTools

could not synthesize a `ToExpr`, `Repr`, or `ToString` instance for type
  List WoodSplittingTool

这是因为 Lean 试图使用内置表中的代码来显示一个列表，但这段代码要求 WoodSplittingTool 的显示代码已经存在。 可以通过指示 Lean 在定义数据类型时生成这段显示代码，而不是在作为 #eval 的一部分的最后时刻才生成，来绕过这个错误；方法是在其定义中添加 deriving Repr：

inductive Firewood where | birch | pine | beech deriving Repr

对 Firewood 的列表求值会成功：

def allFirewood : List Firewood := [ Firewood.birch, Firewood.pine, Firewood.beech ][Firewood.birch, Firewood.pine, Firewood.beech]#eval allFirewood

[Firewood.birch, Firewood.pine, Firewood.beech]