2. 依值类型论（Dependent Type Theory）2. Dependent Type Theory🔗
依值类型论（Dependent Type Theory）是一种强大且富有表现力的语言，它允许你表达复杂的数学断言、编写复杂的硬件和软件规约，并以自然且统一的方式对这两者进行推理。Lean 基于一种称为构造演算（Calculus of Constructions）的依值类型论版本，该版本具有可数的非累积宇宙（Universe）层级结构和归纳类型（Inductive Type）。到本章结束时，你将理解这其中大部分内容的含义。Dependent type theory is a powerful and expressive language, allowing
you to express complex mathematical assertions, write complex hardware
and software specifications, and reason about both of these in a
natural and uniform way. Lean is based on a version of dependent type
theory known as the Calculus of Constructions, with a countable
hierarchy of non-cumulative universes and inductive types. By the end
of this chapter, you will understand much of what this means.
2.1. 简单类型论（Simple Type Theory）2.1. Simple Type Theory🔗
“类型论（Type Theory）”因其每个表达式都有一个关联的类型（Type）而得名。例如，在给定上下文中，x + 0 可能表示一个自然数，而 f 可能表示一个关于自然数的函数。对于喜欢精确定义的人来说，Lean 中的自然数是一个任意精度的无符号整数。“Type theory” gets its name from the fact that every expression has an
associated type. For example, in a given context, x + 0 may
denote a natural number and f may denote a function on the natural
numbers. For those who like precise definitions, a Lean natural number
is an arbitrary-precision unsigned integer.
以下是一些关于如何在 Lean 中声明对象并检查其类型的示例。Here are some examples of how you can declare objects in Lean and
check their types.
任何位于 /- 和 -/ 之间的文本构成一个注释块，被 Lean 忽略。类似地，两个破折号 -- 表示该行其余部分包含注释，同样被忽略。注释块可以嵌套，这使得可以“注释掉”代码块，就像在许多编程语言中一样。Any text between /- and -/ constitutes a comment block that is
ignored by Lean. Similarly, two dashes -- indicate that the rest of
the line contains a comment that is also ignored. Comment blocks can
be nested, making it possible to “comment out” chunks of code, just as
in many programming languages.
def 关键字用于在工作环境中声明新的常量符号。在上面的示例中，def m : Nat := 1 定义了一个新的常量 m，其类型为 Nat，其值为 1。#check 命令要求 Lean 报告这些对象的类型；在 Lean 中，用于查询系统信息的辅助命令通常以井号（#）符号开头。#eval 命令要求 Lean 计算给定的表达式。你应该尝试自己声明一些常量并类型检查一些表达式。以这种方式声明新对象是试验系统的好方法。The def keyword declares new constant symbols into the
working environment. In the example above, def m : Nat := 1
defines a new constant m of type Nat whose value is 1.
The #check command asks Lean to report their
types; in Lean, auxiliary commands that query the system for
information typically begin with the hash (#) symbol.
The #eval command asks Lean to evaluate the given expression.
You should try
declaring some constants and type checking some expressions on your
own. Declaring new objects in this manner is a good way to experiment
with the system.
简单类型论（Simple Type Theory）的强大之处在于你可以从其他类型构建新类型。例如，如果 a 和 b 是类型，则 a -> b 表示从 a 到 b 的函数类型，而 a × b 表示由 a 的一个元素和 b 的一个元素配对而成的类型，也称为笛卡尔积（Cartesian Product）。请注意 × 是一个 Unicode 符号。合理使用 Unicode 可以提高可读性，并且所有现代编辑器都对其有很好的支持。在 Lean 标准库中，你经常看到希腊字母用来表示类型，以及 Unicode 符号 → 作为 -> 的更紧凑版本。What makes simple type theory powerful is that you can build new types
out of others. For example, if a and b are types, a -> b
denotes the type of functions from a to b, and a × b
denotes the type of pairs consisting of an element of a paired
with an element of b, also known as the Cartesian product. Note
that × is a Unicode symbol. The judicious use of Unicode improves
legibility, and all modern editors have great support for it. In the
Lean standard library, you often see Greek letters to denote types,
and the Unicode symbol → as a more compact version of ->.
Nat.succ (n : Nat) : Nat#check Nat.succNat.succ (n : Nat) : Nat
(0, 1) : Nat × Nat#check (0, 1)(0, 1) : Nat × Nat
Nat.add : Nat → Nat → Nat#check Nat.addNat.add : Nat → Nat → Nat
Nat.succ 2 : Nat#check Nat.succ 2Nat.succ 2 : Nat
Nat.add 3 : Nat → Nat#check Nat.add 3Nat.add 3 : Nat → Nat
Nat.add 5 2 : Nat#check Nat.add 5 2Nat.add 5 2 : Nat
(5, 9).fst : Nat#check (5, 9).1(5, 9).fst : Nat
(5, 9).snd : Nat#check (5, 9).2(5, 9).snd : Nat
3#eval Nat.succ 23
7#eval Nat.add 5 27
5#eval (5, 9).15
9#eval (5, 9).29
再一次，你应该自己尝试一些示例。Once again, you should try some examples on your own.
让我们来看一些基本语法。你可以通过输入 \to、\r 或 \-> 来输入 Unicode 箭头 →。你也可以使用 ASCII 替代形式 ->，因此表达式 Nat -> Nat 和 Nat → Nat 表示相同的意思。这两个表达式都表示将一个自然数作为输入并返回一个自然数作为输出的函数类型。笛卡尔积的 Unicode 符号 × 可以通过输入 \times 来输入。你通常会使用小写希腊字母，如 α、β 和 γ，来表示类型变量。你可以分别通过 \a、\b 和 \g 来输入这些特定字母。Let's take a look at some basic syntax. You can enter the Unicode
arrow → by typing \to or \r or \->. You can also use the
ASCII alternative ->, so the expressions Nat -> Nat and Nat → Nat
mean the same thing. Both expressions denote the type of
functions that take a natural number as input and return a natural
number as output. The Unicode symbol × for the Cartesian product
is entered as \times. You will generally use lower-case Greek
letters like α, β, and γ to range over types. You can
enter these particular ones with \a, \b, and \g.
这里还有几点需要注意。首先，函数 f 应用于值 x 表示为 f x（例如 Nat.succ 2）。其次，在书写类型表达式时，箭头是右结合的；例如，Nat.add 的类型是 Nat → Nat → Nat，它等价于 Nat → (Nat → Nat)。因此你可以将 Nat.add 视为一个函数，它接受一个自然数并返回另一个函数，该函数再接受一个自然数并返回一个自然数。在类型论中，这通常比将 Nat.add 视为接受一对自然数作为输入并返回一个自然数作为输出的函数更方便。例如，它允许你“部分应用”函数 Nat.add。上面的示例显示 Nat.add 3 的类型是 Nat → Nat，也就是说，Nat.add 3 返回一个“等待”第二个参数 n 的函数，这与直接写 Nat.add 3 n 等价。There are a few more things to notice here. First, the application of
a function f to a value x is denoted f x (e.g., Nat.succ 2).
Second, when writing type expressions, arrows associate to the right; for
example, the type of Nat.add is Nat → Nat → Nat which is equivalent
to Nat → (Nat → Nat). Thus you can
view Nat.add as a function that takes a natural number and returns
another function that takes a natural number and returns a natural
number. In type theory, this is generally more convenient than
writing Nat.add as a function that takes a pair of natural numbers as
input and returns a natural number as output. For example, it allows
you to “partially apply” the function Nat.add. The example above shows
that Nat.add 3 has type Nat → Nat, that is, Nat.add 3 returns a
function that “waits” for a second argument, n, which is then
equivalent to writing Nat.add 3 n.
你已经看到，如果你有 m : Nat 和 n : Nat，那么 (m, n) 表示 m 和 n 的有序对，其类型为 Nat × Nat。这提供了一种创建自然数对的方法。反过来，如果你有 p : Nat × Nat，那么你可以写 p.1 : Nat 和 p.2 : Nat。这提供了一种提取其两个分量的方法。You have seen that if you have m : Nat and n : Nat, then
(m, n) denotes the ordered pair of m and n which is of
type Nat × Nat. This gives you a way of creating pairs of natural
numbers. Conversely, if you have p : Nat × Nat, then you can write
p.1 : Nat and p.2 : Nat. This gives you a way of extracting
its two components.
2.2. 作为对象的类型（Types as objects）2.2. Types as objects🔗
Lean 的依值类型论扩展简单类型论的一种方式是，类型本身——如 Nat 和 Bool 这样的实体——成为了一等公民，也就是说，它们本身就是对象。为了做到这一点，它们每个也必须有一个类型。One way in which Lean's dependent type theory extends simple type
theory is that types themselves—entities like Nat and Bool—are first-class citizens, which is to say that they themselves are
objects. For that to be the case, each of them also has to have a
type.
你可以看到上面的每个表达式都是类型 Type 的对象。你也可以为类型声明新的常量：You can see that each one of the expressions above is an object of
type Type. You can also declare new constants for types:
如上例所示，你已经看到了一个类型为 Type → Type → Type 的函数示例，即笛卡尔积 Prod：As the example above suggests, you have already seen an example of a function of type
Type → Type → Type, namely, the Cartesian product Prod:
这是另一个例子：给定任意类型 α，类型 List α 表示类型为 α 的元素构成的列表（List）类型。Here is another example: given any type α, the type List α
denotes the type of lists of elements of type α.
既然 Lean 中每个表达式都有一个类型，那么很自然地会问：Type 本身的类型是什么？Given that every expression in Lean has a type, it is natural to ask:
what type does Type itself have?
Type : Type 1#check TypeType : Type 1
你实际上已经遇到了 Lean 类型系统中最微妙的方面之一。Lean 的基础框架具有一个无限的类型层级：You have actually come up against one of the most subtle aspects of
Lean's typing system. Lean's underlying foundation has an infinite
hierarchy of types:
Type : Type 1#check TypeType : Type 1
Type 1 : Type 2#check Type 1Type 1 : Type 2
Type 2 : Type 3#check Type 2Type 2 : Type 3
Type 3 : Type 4#check Type 3Type 3 : Type 4
Type 4 : Type 5#check Type 4Type 4 : Type 5
将 Type 0 视为“小”或“普通”类型的宇宙（Universe）。Type 1 是一个更大的类型宇宙，它包含 Type 0 作为一个元素，而 Type 2 是一个更大的类型宇宙，它包含 Type 1 作为一个元素。这个列表是无限的：对于每个自然数 n，都有一个 Type n。Type 是 Type 0 的缩写：Think of Type 0 as a universe of “small” or “ordinary” types.
Type 1 is then a larger universe of types, which contains Type 0
as an element, and Type 2 is an even larger universe of types,
which contains Type 1 as an element. The list is infinite:
there is a Type n for every natural number n. Type is
an abbreviation for Type 0:
Type : Type 1#check TypeType : Type 1
Type : Type 1#check Type 0Type : Type 1
下表有助于具体化所讨论的关系。沿 x 轴的移动表示宇宙（Universe）的变化，而沿 y 轴的移动表示有时被称为“度（Degree）”的变化。The following table may help concretize the relationships being discussed.
Movement along the x-axis represents a change in the universe, while movement
along the y-axis represents a change in what is sometimes referred to as
“degree”.
sort（种类）sort
| Prop（Sort 0）Prop (Sort 0)
| Type（Sort 1）Type (Sort 1)
| Type 1（Sort 2）Type 1 (Sort 2)
| Type 2（Sort 3）Type 2 (Sort 3)
| ......
|
|---|
type（类型）type
| TrueTrue
| BoolBool
| Nat -> TypeNat -> Type
| Type -> Type 1Type -> Type 1
| ......
|
term（项）term
| True.introTrue.intro
| truetrue
| fun n => Fin nfun n => Fin n
| fun (_ : Type) => Typefun (_ : Type) => Type
| ......
|
然而，某些操作需要跨越类型宇宙（Universe）是多态的（Polymorphic）。例如，List α 对于任何类型 α 都应有意义，无论 α 位于哪个类型宇宙中。这解释了函数 List 的类型签名：Some operations, however, need to be polymorphic over type
universes. For example, List α should make sense for any type
α, no matter which type universe α lives in. This explains the
type signature of the function List:
这里 u 是一个取值范围覆盖类型层级的变量。#check 命令的输出意味着每当 α 具有类型 Type u 时，List α 也具有类型 Type u。函数 Prod 同样是多态的：Here u is a variable ranging over type levels. The output of the
#check command means that whenever α has type Type u,
List α also has type Type u. The function Prod is
similarly polymorphic:
为了定义多态常量，Lean 允许你使用 universe 命令显式声明宇宙（Universe）变量：To define polymorphic constants, Lean allows you to
declare universe variables explicitly using the universe command:
universe u
def F (α : Type u) : Type u := Prod α α
F.{u} (α : Type u) : Type u#check FF.{u} (α : Type u) : Type u
你可以通过定义 F 时提供宇宙参数来避免使用 universe 命令：You can avoid the universe command by providing the universe parameters when defining F:
def F.{u} (α : Type u) : Type u := Prod α α
F.{u} (α : Type u) : Type u#check FF.{u} (α : Type u) : Type u
2.3. 函数抽象与求值（Function Abstraction and Evaluation）2.3. Function Abstraction and Evaluation🔗
Lean 提供了一个 fun（或 λ）关键字，用于从表达式创建函数，如下所示：Lean provides a fun (or λ) keyword to create a function
from an expression as follows:
在这个示例中，类型 Nat 可以被推断出来：The type Nat can be inferred in this example:
你可以通过传递所需的参数来求值一个 lambda（λ）函数：You can evaluate a lambda function by passing the required parameters:
从另一个表达式创建函数的过程称为λ 抽象（Lambda Abstraction）。假设你有一个变量 x : α 并且你可以构造一个表达式 t : β，那么表达式 fun (x : α) => t，或等价地 λ (x : α) => t，是一个类型为 α → β 的对象。将其视为从 α 到 β 的函数，它将任意值 x 映射到值 t。Creating a function from another expression is a process known as
lambda abstraction. Suppose you have the variable x : α and you can
construct an expression t : β, then the expression fun (x : α) => t,
or, equivalently, λ (x : α) => t, is an object of type α → β. Think of
this as the function from α to β which maps
any value x to the value t.
这里还有一些例子Here are some more examples
Lean 将最后三个示例解释为相同的表达式；在最后一个表达式中，Lean 从表达式 if not y then x + 1 else x + 2 推断出 x 和 y 的类型。Lean interprets the final three examples as the same expression; in
the last expression, Lean infers the type of x and y from the
expression if not y then x + 1 else x + 2.
一些数学上常见的函数操作示例可以用λ 抽象（Lambda Abstraction）来描述：Some mathematically common examples of operations of functions can be
described in terms of lambda abstraction:
思考这些表达式的含义。表达式 fun x : Nat => x 表示 Nat 上的恒等函数（Identity Function），表达式 fun x : Nat => true 表示始终返回 true 的常函数（Constant Function），而 fun x : Nat => g (f x) 表示 f 和 g 的复合（Composition）。通常，你可以省略类型标注，让 Lean 为你推断。因此，例如，你可以写 fun x => g (f x) 来代替 fun x : Nat => g (f x)。Think about what these expressions mean. The expression
fun x : Nat => x denotes the identity function on Nat, the
expression fun x : Nat => true denotes the constant function that
always returns true, and fun x : Nat => g (f x) denotes the
composition of f and g. You can, in general, leave off the
type annotation and let Lean infer it for you. So, for example, you
can write fun x => g (f x) instead of fun x : Nat => g (f x).
你可以将函数作为参数传递，并通过为它们命名 f 和 g，然后在实现中使用这些函数：You can pass functions as parameters and by giving them names f
and g you can then use those functions in the implementation:
你也可以将类型作为参数传递：You can also pass types as parameters:
fun α β γ g f x => g (f x) : (α β γ : Type) → (β → γ) → (α → β) → α → γ#check fun (α β γ : Type) (g : β → γ) (f : α → β) (x : α) => g (f x)fun α β γ g f x => g (f x) : (α β γ : Type) → (β → γ) → (α → β) → α → γ
例如，最后一个表达式表示一个函数，它接受三个类型 α、β 和 γ，以及两个函数 g : β → γ 和 f : α → β，并返回 g 和 f 的复合。（理解这个函数的类型需要理解依值积（Dependent Product），这将在下面解释。）The last expression, for example, denotes the function that takes
three types, α, β, and γ, and two functions, g : β → γ
and f : α → β, and returns the composition of g and f.
(Making sense of the type of this function requires an understanding
of dependent products, which will be explained below.)
lambda（λ）表达式的一般形式是 fun (x : α) => t，其中变量 x 是一个“绑定变量（Bound Variable）”：它实际上是一个占位符，其“作用域”不超出表达式 t。例如，表达式 fun (b : β) (x : α) => b 中的变量 b 与之前声明的常量 b 毫无关系。事实上，该表达式表示的函数与 fun (u : β) (z : α) => u 相同。The general form of a lambda expression is fun (x : α) => t, where
the variable x is a “bound variable”: it is really a placeholder,
whose “scope” does not extend beyond the expression t. For
example, the variable b in the expression fun (b : β) (x : α) => b
has nothing to do with the constant b declared earlier. In fact,
the expression denotes the same function as fun (u : β) (z : α) => u.
形式上，在绑定变量重命名下相同的表达式称为α 等价（Alpha Equivalent），并且被认为“相同”。Lean 能够识别这种等价性。Formally, expressions that are the same up to a renaming of bound
variables are called alpha equivalent, and are considered “the
same.” Lean recognizes this equivalence.
注意，将项 t : α → β 应用于项 s : α 会得到表达式 t s : β。回到前面的例子并为了清晰而重命名绑定变量，注意以下表达式的类型：Notice that applying a term t : α → β to a term s : α yields
an expression t s : β. Returning to the previous example and
renaming bound variables for clarity, notice the types of the
following expressions:
正如预期的那样，表达式 (fun x : Nat => x) 1 的类型是 Nat。事实上，更精确地说：将表达式 (fun x : Nat => x) 应用于 1 应该“返回”值 1。而事实上，确实如此：As expected, the expression (fun x : Nat => x) 1 has type Nat.
In fact, more should be true: applying the expression (fun x : Nat => x) to
1 should “return” the value 1. And, indeed, it does:
1#eval (fun x : Nat => x) 11
true#eval (fun unused variable `x`
Note: This linter can be disabled with `set_option linter.unusedVariables false`x : Nat => true) 1true
稍后你将看到这些项是如何求值的。现在，只需注意这是依值类型论的一个重要特征：每个项都具有计算行为，并支持规范化（Normalization）的概念。原则上，归约为相同值的两个项称为定义上相等（Definitionally Equal）。它们被 Lean 的类型检查器视为“相同”，并且 Lean 会尽力识别和支持这种等同。You will see later how these terms are evaluated. For now, notice that
this is an important feature of dependent type theory: every term has
a computational behavior, and supports a notion of normalization. In
principle, two terms that reduce to the same value are called
definitionally equal. They are considered “the same” by Lean's type
checker, and Lean does its best to recognize and support these
identifications.
Lean 是一门完整的编程语言。它具有生成二进制可执行文件的编译器和交互式解释器。你可以使用 #eval 命令来执行表达式，这是测试函数的推荐方式。Lean is a complete programming language. It has a compiler that
generates a binary executable and an interactive interpreter. You can
use the command #eval to execute expressions, and it is the
preferred way of testing your functions.
2.4. 定义（Definitions）2.4. Definitions🔗
回顾一下，def 关键字提供了一种声明新的命名对象的重要方式。Recall that the def keyword provides one important way of declaring new named
objects.
def double (x : Nat) : Nat :=
x + x
如果你了解函数在其他编程语言中的工作方式，这看起来可能会更熟悉。名称 double 被定义为一个函数，它接受一个类型为 Nat 的输入参数 x，调用的结果是 x + x，因此返回类型是 Nat。然后你可以使用以下方式调用这个函数：This might look more familiar to you if you know how functions work in
other programming languages. The name double is defined as a
function that takes an input parameter x of type Nat, where the
result of the call is x + x, so it is returning type Nat. You
can then invoke this function using:
在这种情况下，你可以将 def 视为一种命名的 fun。以下产生相同的结果：In this case you can think of def as a kind of named fun.
The following yields the same result:
def double : Nat → Nat :=
fun x => x + x
6#eval double 36
当 Lean 有足够的信息时，你可以省略类型声明。类型推断（Type Inference）是 Lean 的重要组成部分：You can omit the type declarations when Lean has enough information to
infer it. Type inference is an important part of Lean:
def double :=
fun (x : Nat) => x + x
定义的一般形式是 def foo : α := bar，其中 α 是表达式 bar 返回的类型。Lean 通常可以推断出类型 α，但显式写出它通常是一个好主意。这明确了你的意图，并且如果定义的右侧没有匹配的类型，Lean 将标记错误。The general form of a definition is def foo : α := bar where
α is the type returned from the expression bar. Lean can
usually infer the type α, but it is often a good idea to write it
explicitly. This clarifies your intention, and Lean will flag an
error if the right-hand side of the definition does not have a matching
type.
右侧 bar 可以是任何表达式，而不仅仅是 lambda。因此 def 也可以用于简单地命名一个值，就像这样：The right hand side bar can be any expression, not just a lambda.
So def can also be used to simply name a value like this:
def pi := 3.141592654
def 可以接受多个输入参数。让我们创建一个将两个自然数相加的函数：def can take multiple input parameters. Let's create one
that adds two natural numbers:
def add (x y : Nat) :=
x + y
5#eval add 3 25
参数列表可以这样分隔：The parameter list can be separated like this:
def double (x : Nat) : Nat :=
x + x
def add (x : Nat) (y : Nat) :=
x + y
22#eval add (double 3) (7 + 9)22
注意，这里我们调用了 double 函数来创建传递给 add 的第一个参数。Notice here we called the double function to create the first
parameter to add.
你可以在 def 内部使用其他更有趣的表达式：You can use other more interesting expressions inside a def:
你可能能猜到这将做什么。You can probably guess what this one will do.
你也可以定义一个将另一个函数作为输入的函数。以下函数将给定的函数调用两次，将第一次调用的输出传递给第二次：You can also define a function that takes another function as input.
The following calls a given function twice passing the output of the
first invocation to the second:
def double (x : Nat) : Nat :=
x + x
def doTwice (f : Nat → Nat) (x : Nat) : Nat :=
f (f x)
8#eval doTwice double 28
现在，为了更抽象一些，你也可以指定像类型参数这样的参数：Now to get a bit more abstract, you can also specify arguments that
are like type parameters:
def compose (α β γ : Type) (g : β → γ) (f : α → β) (x : α) : γ :=
g (f x)
这意味着 compose 是一个接受任意两个函数作为输入参数的函数，只要这些函数各自只接受一个输入。类型代数 β → γ 和 α → β 意味着第二个函数的输出类型必须与第一个函数的输入类型匹配——这很合理，否则这两个函数将不可复合。This means compose is a function that takes any two functions as input
arguments, so long as those functions each take only one input.
The type algebra β → γ and α → β means it is a requirement
that the type of the output of the second function must match the
type of the input to the first function—which makes sense, otherwise
the two functions would not be composable.
compose 还接受一个类型为 α 的第三个参数，它使用这个参数来调用第二个函数（局部命名为 f），并将该函数的结果（类型为 β）作为输入传递给第一个函数（局部命名为 g）。第一个函数返回类型 γ，因此这也是 compose 函数的返回类型。compose also takes a 3rd argument of type α which
it uses to invoke the second function (locally named f) and it
passes the result of that function (which is type β) as input to the
first function (locally named g). The first function returns a type
γ so that is also the return type of the compose function.
compose 也非常通用，它可以处理任何类型 α β γ。这意味着只要两个函数各自接受一个参数，并且第二个函数的输出类型与第一个函数的输入类型匹配，compose 就可以复合几乎任何两个函数。例如：compose is also very general in that it works over any type
α β γ. This means compose can compose just about any 2 functions
so long as they each take one parameter, and so long as the type of
output of the second matches the input of the first. For example:
def compose (α β γ : Type) (g : β → γ) (f : α → β) (x : α) : γ :=
g (f x)
def double (x : Nat) : Nat :=
x + x
def square (x : Nat) : Nat :=
x * x
18#eval compose Nat Nat Nat double square 318
2.5. 局部定义（Local Definitions）2.5. Local Definitions🔗
Lean 还允许你使用 let 关键字引入“局部”定义。表达式 let a := t1; t2 在定义上等价于将 t2 中的每个 a 替换为 t1 后得到的结果。Lean also allows you to introduce “local” definitions using the
let keyword. The expression let a := t1; t2 is
definitionally equal to the result of replacing every occurrence of
a in t2 by t1.
这里，twice_double x 在定义上等价于项 (x + x) * (x + x)。Here, twice_double x is definitionally equal to the term (x + x) * (x + x).
你可以通过链式使用 let 语句来组合多个赋值：You can combine multiple assignments by chaining let statements:
let y := 2 + 2;
let z := y + y;
z * z : Nat#check let y := 2 + 2; let z := y + y; z * zlet y := 2 + 2;
let z := y + y;
z * z : Nat
64#eval let y := 2 + 2; let z := y + y; z * z64
当使用换行时，; 可以省略。The ; can be omitted when a line break is used.
def t (x : Nat) : Nat :=
let y := x + x
y * y
注意，表达式 let a := t1; t2 的含义与 (fun a => t2) t1 的含义非常相似，但两者并不相同。在第一个表达式中，你应该将 t2 中 a 的每个出现视为 t1 的语法缩写。在第二个表达式中，a 是一个变量，表达式 fun a => t2 必须独立于 a 的值而具有意义。let 结构是一种更强的缩写方式，并且存在某些形式为 let a := t1; t2 的表达式无法表示为 (fun a => t2) t1。作为练习，试着理解为什么下面的 foo 定义可以通过类型检查，而 bar 的定义却不能。Notice that the meaning of the expression let a := t1; t2 is very
similar to the meaning of (fun a => t2) t1, but the two are not
the same. In the first expression, you should think of every instance
of a in t2 as a syntactic abbreviation for t1. In the
second expression, a is a variable, and the expression
fun a => t2 has to make sense independently of the value of a.
The let construct is a stronger means of abbreviation, and there
are expressions of the form let a := t1; t2 that cannot be
expressed as (fun a => t2) t1. As an exercise, try to understand
why the definition of foo below type checks, but the definition of
bar does not.
def foo := let a := Nat; fun x : a => x + 2
/-
def bar := (fun a => fun x : a => x + 2) Nat
-/
2.6. 变量与段（Variables and Sections）2.6. Variables and Sections🔗
考虑以下三个函数定义：Consider the following three function definitions:
def compose (α β γ : Type) (g : β → γ) (f : α → β) (x : α) : γ :=
g (f x)
def doTwice (α : Type) (h : α → α) (x : α) : α :=
h (h x)
def doThrice (α : Type) (h : α → α) (x : α) : α :=
h (h (h x))
Lean 为你提供了 variable 命令，使这样的声明看起来更紧凑：Lean provides you with the variable command to make such
declarations look more compact:
variable (α β γ : Type)
def compose (g : β → γ) (f : α → β) (x : α) : γ :=
g (f x)
def doTwice (h : α → α) (x : α) : α :=
h (h x)
def doThrice (h : α → α) (x : α) : α :=
h (h (h x))
你可以声明任何类型的变量，而不仅仅是 Type 本身：You can declare variables of any type, not just Type itself:
variable (α β γ : Type)
variable (g : β → γ) (f : α → β) (h : α → α)
variable (x : α)
def compose := g (f x)
def doTwice := h (h x)
def doThrice := h (h (h x))
def compose : (α β γ : Type) → (β → γ) → (α → β) → α → γ :=
fun α β γ g f x => g (f x)#print composedef compose : (α β γ : Type) → (β → γ) → (α → β) → α → γ :=
fun α β γ g f x => g (f x)
def doTwice : (α : Type) → (α → α) → α → α :=
fun α h x => h (h x)#print doTwicedef doTwice : (α : Type) → (α → α) → α → α :=
fun α h x => h (h x)
def doThrice : (α : Type) → (α → α) → α → α :=
fun α h x => h (h (h x))#print doThricedef doThrice : (α : Type) → (α → α) → α → α :=
fun α h x => h (h (h x))
将它们打印出来显示，所有三组定义具有完全相同的效果。Printing them out shows that all three groups of definitions have
exactly the same effect.
variable 命令指示 Lean 将声明的变量作为绑定变量插入到引用它们的定义中。Lean 足够智能，能够找出哪些变量在定义中被显式或隐式地使用。因此，你在编写定义时可以将 α、β、γ、g、f、h 和 x 视为固定对象，然后让 Lean 自动为你抽象定义。The variable command instructs Lean to insert the declared
variables as bound variables in definitions that refer to them by
name. Lean is smart enough to figure out which variables are used
explicitly or implicitly in a definition. You can therefore proceed as
though α, β, γ, g, f, h, and x are fixed
objects when you write your definitions, and let Lean abstract the
definitions for you automatically.
以这种方式声明时，变量将保持有效直到当前文件末尾。然而，有时限制变量的作用域是有用的。为此，Lean 提供了 section 的概念：When declared in this way, a variable stays in scope until the end of
the file you are working on. Sometimes, however, it is useful to limit
the scope of a variable. For that purpose, Lean provides the notion of
a section:
section useful
variable (α β γ : Type)
variable (g : β → γ) (f : α → β) (h : α → α)
variable (x : α)
def compose := g (f x)
def doTwice := h (h x)
def doThrice := h (h (h x))
end useful
当段（Section）关闭时，变量将超出作用域，无法再被引用。When the section is closed, the variables go out of scope, and cannot
be referenced any more.
你不必缩进段内的行。也不必为段命名，也就是说，你可以使用匿名的 section / end 对。但是，如果你确实命名了一个段，则必须使用相同的名称来关闭它。段也可以嵌套，这允许你逐步声明新的变量。You do not have to indent the lines within a section. Nor do you have
to name a section, which is to say, you can use an anonymous
section / end pair. If you do name a section, however, you
have to close it using the same name. Sections can also be nested,
which allows you to declare new variables incrementally.
2.7. 命名空间（Namespaces）2.7. Namespaces🔗
Lean 为你提供了将定义分组到嵌套的、层次化的命名空间（Namespace）中的能力：Lean provides you with the ability to group definitions into nested,
hierarchical namespaces:
当你声明在命名空间 Foo 中工作时，你声明的每个标识符都有一个以 “Foo.” 为前缀的全名。在命名空间内部，你可以使用较短的名字来引用标识符，但一旦结束命名空间，你就必须使用较长的名字。与 section 不同，命名空间需要名称。在根级别只有一个匿名命名空间。When you declare that you are working in the namespace Foo, every
identifier you declare has a full name with prefix “Foo.”. Within
the namespace, you can refer to identifiers by their shorter names,
but once you end the namespace, you have to use the longer names.
Unlike section, namespaces require a name. There is only one
anonymous namespace at the root level.
open 命令将较短的名字引入当前上下文。通常，当你导入一个模块时，你会希望打开它所包含的一个或多个命名空间，以便使用较短的标识符。但有时你希望将这些信息保留在完全限定名称的保护下，例如当它们与你想使用的另一个命名空间中的标识符冲突时。因此，命名空间为你提供了一种管理工作环境中名称的方法。The open command brings the shorter names into the current
context. Often, when you import a module, you will want to open one or
more of the namespaces it contains, to have access to the short
identifiers. But sometimes you will want to leave this information
protected by a fully qualified name, for example, when they conflict
with identifiers in another namespace you want to use. Thus namespaces
give you a way to manage names in your working environment.
例如，Lean 将涉及列表（List）的定义和定理分组到命名空间 List 中。For example, Lean groups definitions and theorems involving lists into
a namespace List.
命令 open List 允许你使用较短的名称：The command open List allows you to use the shorter names:
与段（Section）类似，命名空间可以嵌套：Like sections, namespaces can be nested:
已关闭的命名空间可以在之后重新打开，甚至在另一个文件中也可以：Namespaces that have been closed can later be reopened, even in another file:
与段（Section）一样，嵌套的命名空间必须按照打开的顺序关闭。命名空间和段服务于不同的目的：命名空间组织数据，而段声明变量以插入到定义中。段也适用于界定诸如 set_option 和 open 等命令的作用域。Like sections, nested namespaces have to be closed in the order they
are opened. Namespaces and sections serve different purposes:
namespaces organize data and sections declare variables for insertion
in definitions. Sections are also useful for delimiting the scope of
commands such as set_option and open.
然而，在许多方面，namespace ... end 块的行为与 section ... end 块相同。特别地，如果你在命名空间内使用 variable 命令，其作用域仅限于该命名空间。类似地，如果你在命名空间内使用 open 命令，其效果在命名空间关闭时消失。In many respects, however, a namespace ... end block behaves the
same as a section ... end block. In particular, if you use the
variable command within a namespace, its scope is limited to the
namespace. Similarly, if you use an open command within a
namespace, its effects disappear when the namespace is closed.
2.8. 什么使依值类型论成为依值的？（What makes dependent type theory dependent?）2.8. What makes dependent type theory dependent?🔗
简短的解释是：类型可以依赖于参数。你已经看到了一个好例子：类型 List α 依赖于参数 α，而这种依赖性正是区分 List Nat 和 List Bool 的原因。另一个例子，考虑类型 Vector α n，它是长度为 n 的 α 类型元素的向量（Vector）类型。这个类型依赖于两个参数：向量中元素的类型（α : Type）和向量的长度 n : Nat。The short explanation is that types can depend on parameters. You
have already seen a nice example of this: the type List α depends
on the argument α, and this dependence is what distinguishes
List Nat and List Bool. For another example, consider the
type Vector α n, the type of vectors of elements of α of
length n. This type depends on two parameters: the type of the
elements in the vector (α : Type) and the length of the vector
n : Nat.
假设你想写一个函数 cons，它在列表的头部插入一个新元素。cons 应该有什么类型呢？这样的函数是多态的（Polymorphic）：你期望 Nat、Bool 或任意类型 α 的 cons 函数行为方式相同。因此，将类型作为 cons 的第一个参数是有意义的，这样对于任何类型 α，cons α 就是针对 α 类型列表的插入函数。换句话说，对于每个 α，cons α 是一个接受元素 a : α 和列表 as : List α 并返回一个新列表的函数，因此你有 cons α a as : List α。Suppose you wish to write a function cons which inserts a new
element at the head of a list. What type should cons have? Such a
function is polymorphic: you expect the cons function for
Nat, Bool, or an arbitrary type α to behave the same way.
So it makes sense to take the type to be the first argument to
cons, so that for any type, α, cons α is the insertion
function for lists of type α. In other words, for every α,
cons α is the function that takes an element a : α and a list
as : List α, and returns a new list, so you have cons α a as : List α.
显然，cons α 的类型应该是 α → List α → List α。但是 cons 本身应该有什么类型呢？最初猜测可能是 Type → α → List α → List α，但仔细想想，这说不通：这个表达式中的 α 不指向任何东西，而它应该指向类型为 Type 的参数。换句话说，假设 α : Type 是函数的第一个参数，那么接下来两个元素的类型是 α 和 List α。这些类型根据第一个参数 α 而变化。It is clear that cons α should have type α → List α → List α.
But what type should cons have? A first guess might be
Type → α → List α → List α, but, on reflection, this does not make
sense: the α in this expression does not refer to anything,
whereas it should refer to the argument of type Type. In other
words, assuming α : Type is the first argument to the function,
the type of the next two elements are α and List α. These
types vary depending on the first argument, α.
这就是一个依值函数类型（Dependent Function Type），或称依值箭头类型的实例。给定 α : Type 和 β : α → Type，将 β 视为 α 上的一个类型族（Family of Types），也就是说，对于每个 a : α，都有一个类型 β a。在这种情况下，类型 (a : α) → β a 表示函数 f 的类型，其性质是对于每个 a : α，f a 是 β a 的一个元素。换句话说，f 返回的值的类型取决于其输入。This is an instance of a dependent function type, or dependent
arrow type. Given α : Type and β : α → Type, think of β
as a family of types over α, that is, a type β a for each
a : α. In that case, the type (a : α) → β a denotes the type
of functions f with the property that, for each a : α, f a
is an element of β a. In other words, the type of the value
returned by f depends on its input.
注意，(a : α) → β 对于任何表达式 β : Type 都是有意义的。当 β 的值依赖于 a 时（例如上一段中的表达式 β a），(a : α) → β 表示一个依值函数类型。当 β 不依赖于 a 时，(a : α) → β 与类型 α → β 没有区别。事实上，在依值类型论（以及 Lean）中，α → β 只是当 β 不依赖于 a 时 (a : α) → β 的记法。Notice that (a : α) → β makes sense for any expression β : Type.
When the value of β depends on a (as does, for
example, the expression β a in the previous paragraph),
(a : α) → β denotes a dependent function type. When β doesn't
depend on a, (a : α) → β is no different from the type
α → β. Indeed, in dependent type theory (and in Lean), α → β
is just notation for (a : α) → β when β does not depend on a.
回到列表的例子，你可以使用 #check 命令检查以下 List 函数的类型。@ 符号以及圆括号和花括号之间的区别将在稍后解释。Returning to the example of lists, you can use the command #check to
inspect the type of the following List functions. The @ symbol
and the difference between the round and curly braces will be
explained momentarily.
正如依值函数类型 (a : α) → β a 通过允许 β 依赖于 a 来推广函数类型 α → β 的概念一样，依值笛卡尔积类型 (a : α) × β a 以同样的方式推广笛卡尔积 α × β。依值积（Dependent Product）也称为sigma（Σ）类型，你也可以将其写为 Σ a : α, β a。你可以使用 ⟨a, b⟩ 或 Sigma.mk a b 来创建一个依值对（Dependent Pair）。⟨ 和 ⟩ 字符可以分别通过输入 \langle 和 \rangle 或 \< 和 \> 来输入。Just as dependent function types (a : α) → β a generalize the
notion of a function type α → β by allowing β to depend on
a, dependent Cartesian product types (a : α) × β a generalize
the Cartesian product α × β in the same way. Dependent products
are also called sigma types, and you can also write them as
Σ a : α, β a. You can use ⟨a, b⟩ or Sigma.mk a b to create a
dependent pair. The ⟨ and ⟩ characters may be typed with
\langle and \rangle or \< and \>, respectively.
universe u v
def f (α : Type u) (β : α → Type v) (a : α) (b : β a) : (a : α) × β a :=
⟨a, b⟩
def g (α : Type u) (β : α → Type v) (a : α) (b : β a) : Σ a : α, β a :=
Sigma.mk a b
def h1 (x : Nat) : Nat :=
(f Type (fun α => α) Nat x).2
5#eval h1 55
def h2 (x : Nat) : Nat :=
(g Type (fun α => α) Nat x).2
5#eval h2 55
上面的函数 f 和 g 表示相同的函数。The functions f and g above denote the same function.
2.9. 隐式参数（Implicit Arguments）2.9. Implicit Arguments🔗
假设我们有一个如下的列表实现：Suppose we have an implementation of lists as:
然后，你可以按如下方式构造 Nat 的列表：Then, you can construct lists of Nat as follows:
由于构造器（Constructor）在类型上是多态的，我们必须反复插入类型 Nat 作为参数。但这个信息是冗余的：我们可以从 Lst.cons Nat 5 (Lst.nil Nat) 中推断出参数 α，因为第二个参数 5 的类型是 Nat。类似地，我们可以在 Lst.nil Nat 中推断出参数，不是从该表达式中的其他任何东西，而是从它作为参数传递给函数 Lst.cons 这一事实，而 Lst.cons 在该位置期望一个类型为 Lst α 的元素。Because the constructors are polymorphic over types, we have to insert
the type Nat as an argument repeatedly. But this information is
redundant: one can infer the argument α in
Lst.cons Nat 5 (Lst.nil Nat) from the fact that the second argument, 5, has
type Nat. One can similarly infer the argument in Lst.nil Nat, not
from anything else in that expression, but from the fact that it is
sent as an argument to the function Lst.cons, which expects an element
of type Lst α in that position.
这是依值类型论的一个核心特征：项携带大量信息，并且通常其中一些信息可以从上下文中推断出来。在 Lean 中，使用下划线 _ 来指定系统应自动填入该信息。这被称为“隐式参数（Implicit Argument）”。This is a central feature of dependent type theory: terms carry a lot
of information, and often some of that information can be inferred
from the context. In Lean, one uses an underscore, _, to specify
that the system should fill in the information automatically. This is
known as an “implicit argument.”
然而，输入所有这些下划线仍然很繁琐。当一个函数接受一个通常可以从上下文中推断出来的参数时，Lean 允许你指定该参数默认保持为隐式的。这通过将参数放在花括号中来实现，如下所示：It is still tedious, however, to type all these underscores. When a
function takes an argument that can generally be inferred from
context, Lean allows you to specify that this argument should, by
default, be left implicit. This is done by putting the arguments in
curly braces, as follows:
唯一的变化是在变量声明中 α : Type u 周围加上了花括号。我们也可以在函数定义中使用这种手段：All that has changed are the braces around α : Type u in the
declaration of the variables. We can also use this device in function
definitions:
universe u
def ident {α : Type u} (x : α) := x
检查 ident 的类型需要将其括在括号中以避免显示其签名：Checking the type of ident requires wrapping it in parentheses to avoid having its signature shown:
universe u
def ident {α : Type u} (x : α) := x
ident : ?m.1 → ?m.1#check (ident)ident : ?m.1 → ?m.1
ident 1 : Nat#check ident 1ident 1 : Nat
ident "hello" : String#check ident "hello"ident "hello" : String
@ident : {α : Type u_1} → α → α#check @ident@ident : {α : Type u_1} → α → α
这使得 ident 的第一个参数变为隐式。在记法上，这隐藏了类型的指定，使得 ident 看起来只接受一个任意类型的参数。事实上，标准库中的函数 id 正是以这种方式定义的。我们在这里选择了一个非传统的名称，仅仅是为了避免名称冲突。The makes the first argument to ident implicit. Notationally,
this hides the specification of the type, making it look as though
ident simply takes an argument of any type. In fact, the function
id is defined in the standard library in exactly this way. We have
chosen a nontraditional name here only to avoid a clash of names.
当使用 variable 命令声明变量时，也可以将其指定为隐式：Variables can also be specified as implicit when they are declared with
the variable command:
这里的 ident 定义与上面的定义具有相同的效果。This definition of ident here has the same effect as the one
above.
Lean 具有非常复杂的机制来实例化隐式参数，我们将看到它们可以用来推断函数类型、谓词（Predicate）甚至证明（Proof）。在项中实例化这些“洞（Hole）”或“占位符（Placeholder）”的过程通常称为精化（Elaboration）。隐式参数的存在意味着有时可能没有足够的信息来精确确定一个表达式的含义。像 id 或 List.nil 这样的表达式被称为多态的（Polymorphic），因为它在不同上下文中可以具有不同含义。Lean has very complex mechanisms for instantiating implicit arguments,
and we will see that they can be used to infer function types,
predicates, and even proofs. The process of instantiating these
“holes,” or “placeholders,” in a term is often known as
elaboration. The presence of implicit arguments means that at times
there may be insufficient information to fix the meaning of an
expression precisely. An expression like id or List.nil is
said to be polymorphic, because it can take on different meanings in
different contexts.
你可以通过写 (e : T) 来指定表达式 e 的类型 T。这会指示 Lean 的精化器（Elaborator）在尝试解析隐式参数时使用 T 作为 e 的类型。在下面的第二对示例中，这种机制用于指定表达式 id 和 List.nil 的所需类型：One can always specify the type T of an expression e by
writing (e : T). This instructs Lean's elaborator to use the value
T as the type of e when trying to resolve implicit
arguments. In the second pair of examples below, this mechanism is
used to specify the desired types of the expressions id and
List.nil:
数字字面量（Numeral）在 Lean 中是重载的，但当无法推断数字字面量的类型时，Lean 默认假定它是一个自然数。因此，下面前两个 #check 命令中的表达式以相同方式精化，而第三个 #check 命令将 2 解释为整数。Numerals are overloaded in Lean, but when the type of a numeral cannot
be inferred, Lean assumes, by default, that it is a natural number. So
the expressions in the first two #check commands below are
elaborated in the same way, whereas the third #check command
interprets 2 as an integer.
然而，有时我们可能会遇到这样的情况：我们已将函数的某个参数声明为隐式，但现在想要显式提供该参数。如果 foo 是这样一个函数，那么记法 @foo 表示将所有参数都变为显式的同一函数。Sometimes, however, we may find ourselves in a situation where we have
declared an argument to a function to be implicit, but now want to
provide the argument explicitly. If foo is such a function, the
notation @foo denotes the same function with all the arguments
made explicit.
注意，现在第一个 #check 命令给出了标识符 id 的类型，没有插入任何占位符。此外，输出表明第一个参数是隐式的。Notice that now the first #check command gives the type of the
identifier, id, without inserting any placeholders. Moreover, the
output indicates that the first argument is implicit.
