6.1. 消息（Messages）6.1. Messages🔗

Lean 产生三种消息：Lean produces three kinds of messages:

Errors

当代码中存在不一致导致无法处理时，会产生错误（Error）。例如语法错误（如缺少 )）和类型错误（type error），如试图将自然数（natural number）与函数相加。Errors are produced when an inconsistency in the code means that it can't be processed. Examples include syntax errors (e.g. a missing )) and type errors such as attempting to add a natural number to a function.

Warnings

警告（Warning）描述代码的潜在问题，例如存在 sorry。与错误不同，代码并非无意义；然而，警告需要仔细关注。Warnings describe potential problems with the code, such as the presence of sorry. Unlike with errors, the code is not meaningless; however, warnings deserve careful attention.

Information

信息（Information）不指示代码的任何问题，包括来自诸如 #check 和 #eval 等命令的输出。Information doesn't indicate any problem with the code, and includes output from commands such as #check and #eval.

Lean 可以检查命令是否产生了预期的消息。如果消息匹配，则忽略任何错误；这可用于确保出现了正确的错误。如果不匹配，则会产生错误。你可以使用 #guard_msgs 命令来指定预期的消息。Lean can check that a command produces the expected messages. If the messages match, then any errors are disregarded; this can be used to ensure that the right errors occur. If they don't, an error is produced. You can use the #guard_msgs command to indicate which messages are expected.

以下是一个示例：Here is an example:

在 #guard_msgs 后面的括号中包含消息类别，使其仅检查指定类别，而让其他类别通过。在此示例中，#eval 由于存在 sorry 而发出错误，但为 sorry 始终发出的警告照常显示：Including a message category in parentheses after #guard_msgs causes it to check only the specified category, letting others through. In this example, #eval issues an error due to the presence of sorry, but the warning that is always issued for sorry is displayed as usual:

declaration uses 'sorry'

没有配置时，两条消息都会被捕获：Without the configuration, both messages are captured:

❌️ Docstring on `#guard_msgs` does not match generated message:

- error: aborting evaluation since the expression depends on the
- 'sorry' axiom, which can lead to runtime instability and crashes.
+ warning: declaration uses 'sorry'
+ ---
+ error: aborting evaluation since the expression depends on the 'sorry' axiom, which can lead to runtime instability and crashes.
 
- To attempt to evaluate anyway despite the risks, use the '#eval!'
- command.
- ---
- warning: declaration uses 'sorry'
+ To attempt to evaluate anyway despite the risks, use the '#eval!' command.

本书中的一些示例使用 #guard_msgs 来指示预期的错误。Some examples in this book use #guard_msgs to indicate expected errors.

6.2. 导入文件（Importing Files）6.2. Importing Files🔗

Lean 前端的目的是解释用户输入，构造形式表达式（formal expression），并检查它们是否良构（well-formed）且类型正确（type-correct）。Lean 还支持使用多种编辑器，提供持续检查和反馈。更多信息可以在 Lean 文档页面上找到。The goal of Lean's front end is to interpret user input, construct formal expressions, and check that they are well-formed and type-correct. Lean also supports the use of various editors, which provide continuous checking and feedback. More information can be found on the Lean documentation pages.

Lean 标准库中的定义（definition）和定理（theorem）分布在多个文件中。用户可能还需要使用额外的库，或在多个文件中开发自己的项目。Lean 启动时会自动导入 Init 文件夹的内容，其中包含许多基本定义和构造。因此，我们在此展示的大多数示例都可以“开箱即用”。The definitions and theorems in Lean's standard library are spread across multiple files. Users may also wish to make use of additional libraries, or develop their own projects across multiple files. When Lean starts, it automatically imports the contents of the library Init folder, which includes a number of fundamental definitions and constructions. As a result, most of the examples we present here work “out of the box.”

但是，如果你想使用额外的文件，则需要通过在文件开头的 import 语句手动导入。该命令If you want to use additional files, however, they need to be imported manually, via an import statement at the beginning of a file. The command

import Bar.Baz.Blahimport Bar.Baz.Blah

导入文件 Bar/Baz/Blah.olean，其中描述相对于 Lean 搜索路径（search path）进行解释。关于搜索路径如何确定的信息可以在文档页面上找到。默认情况下，它包括标准库目录，以及（在某些情况下）用户本地项目的根目录。imports the file Bar/Baz/Blah.olean, where the descriptions are interpreted relative to the Lean search path. Information as to how the search path is determined can be found on the documentation pages. By default, it includes the standard library directory, and (in some contexts) the root of the user's local project.

导入是传递的（transitive）。换句话说，如果你导入 Foo，而 Foo 导入了 Bar，那么你也可以访问 Bar 的内容，无需显式导入它。Importing is transitive. In other words, if you import Foo and Foo imports Bar, then you also have access to the contents of Bar, and do not need to import it explicitly.

6.3. 更多关于章节（Sections）6.3. More on Sections🔗

Lean 提供了多种章节机制来帮助组织理论。你在变量与章节（Variables and Sections）中看到，section 命令不仅可以将在逻辑上属于一起的理论元素分组，还可以声明变量（variable），这些变量会根据需要作为参数插入到定理和定义中。请记住，variable 命令的目的是声明用于定理的变量，如下例所示：Lean provides various sectioning mechanisms to help structure a theory. You saw in Variables and Sections that the section command makes it possible not only to group together elements of a theory that go together, but also to declare variables that are inserted as arguments to theorems and definitions, as necessary. Remember that the point of the variable command is to declare variables for use in theorems, as in the following example:

double y : Nat

double (2 * x) : Nat

t1 y : ∀ (y_1 : Nat), double (y + y_1) = double y + double y_1

t1 (2 * x) : ∀ (y : Nat), double (2 * x + y) = double (2 * x) + double y

double 的定义不必将 x 声明为参数；Lean 会自动检测依赖关系并插入它。类似地，Lean 会检测 t1 和 t2 中出现的 x，并自动将其插入。注意，double 并没有将 y 作为参数。变量只包含在实际使用它们的声明中。The definition of double does not have to declare x as an argument; Lean detects the dependence and inserts it automatically. Similarly, Lean detects the occurrence of x in t1 and t2, and inserts it automatically there, too. Note that double does not have y as argument. Variables are only included in declarations where they are actually used.

6.4. 更多关于命名空间（Namespaces）6.4. More on Namespaces🔗

在 Lean 中，标识符由分层名称（name）给出，例如 Foo.Bar.baz。我们在命名空间（Namespaces）中看到，Lean 提供了处理分层名称的机制。命令 namespace Foo 会导致 Foo 被添加到每个定义和定理的名称前，直到遇到 end Foo。命令 open Foo 会为以前缀 Foo 开头的定义和定理创建临时的别名（alias）。In Lean, identifiers are given by hierarchical names like Foo.Bar.baz. We saw in Namespaces that Lean provides mechanisms for working with hierarchical names. The command namespace Foo causes Foo to be prepended to the name of each definition and theorem until end Foo is encountered. The command open Foo then creates temporary aliases to definitions and theorems that begin with prefix Foo.

Foo.bar : Nat

Foo.bar : Nat

以下定义The following definition

被视为宏（macro），展开为is treated as a macro, and expands to

虽然定理和定义的名称必须是唯一的，但标识它们的别名不必如此。当我们打开一个命名空间时，标识符可能产生歧义。Lean 会尝试使用类型信息来根据上下文消歧义，但你始终可以通过给出完整名称来消歧义。为此，字符串 _root_ 是对空前缀的显式描述。Although the names of theorems and definitions have to be unique, the aliases that identify them do not. When we open a namespace, an identifier may be ambiguous. Lean tries to use type information to disambiguate the meaning in context, but you can always disambiguate by giving the full name. To that end, the string _root_ is an explicit description of the empty prefix.

String.add (a b : String) : String

Bool.add (a b : Bool) : Bool

_root_.add (α β : Type) : Type

"hello".add "world" : String

true.add false : Bool

_root_.add Nat Nat : Type

我们可以通过使用 protected 关键字来阻止创建较短的别名：We can prevent the shorter alias from being created by using the protected keyword:

Foo.bar : Nat

这通常用于像 Nat.rec 和 Nat.recOn 这样的名称，以防止常见名称的重载。This is often used for names like Nat.rec and Nat.recOn, to prevent overloading of common names.

open 命令有多种变体。命令The open command admits variations. The command

Nat.zero : Nat

3

仅为列出的标识符创建别名。命令creates aliases for only the identifiers listed. The command

Nat.zero : Nat

3

为 Nat 命名空间中的除列出的标识符之外的所有内容创建别名。creates aliases for everything in the Nat namespace except the identifiers listed.

7

创建将 Nat.mul 重命名为 times、Nat.add 重命名为 plus 的别名。creates aliases renaming Nat.mul to times and Nat.add to plus.

有时将别名从一个命名空间export 到另一个命名空间或导出到顶层是很有用的。命令It is sometimes useful to export aliases from one namespace to another, or to the top level. The command

在当前命名空间中为 succ、add 和 sub 创建别名，因此每当该命名空间被打开时，这些别名都可用。如果此命令在命名空间外部使用，则别名将被导出到顶层。creates aliases for succ, add, and sub in the current namespace, so that whenever the namespace is open, these aliases are available. If this command is used outside a namespace, the aliases are exported to the top level.

6.5. 属性（Attributes）6.5. Attributes🔗

Lean 的主要功能是将用户输入翻译为形式表达式（formal expression），由内核（kernel）检查其正确性，然后存储在环境（environment）中供以后使用。但有些命令对环境有其他影响，要么为环境中的对象分配属性（attribute），要么定义记号（notation），要么声明类型类（type class）的实例，如类型类（type classes）一章所述。这些命令大多具有全局效果，也就是说，它们不仅在当前文件中有效，在导入该文件的任何文件中也都有效。然而，此类命令通常支持 local 修饰符，指示它们仅在当前 section 或 namespace 关闭之前或当前文件结束之前有效。The main function of Lean is to translate user input to formal expressions that are checked by the kernel for correctness and then stored in the environment for later use. But some commands have other effects on the environment, either assigning attributes to objects in the environment, defining notation, or declaring instances of type classes, as described in the chapter on type classes. Most of these commands have global effects, which is to say, they remain in effect not only in the current file, but also in any file that imports it. However, such commands often support the local modifier, which indicates that they only have effect until the current section or namespace is closed, or until the end of the current file.

在使用化简器（Using the Simplifier）中，我们看到可以用 [simp] 属性注解定理，使其可供化简器（simplifier）使用。以下示例定义了列表上的前缀关系，证明了该关系是自反的（reflexive），并给该定理分配了 [simp] 属性。In Using the Simplifier, we saw that theorems can be annotated with the [simp] attribute, which makes them available for use by the simplifier. The following example defines the prefix relation on lists, proves that this relation is reflexive, and assigns the [simp] attribute to that theorem.

然后化简器通过将其重写（rewrite）为 True 来证明 isPrefix [1, 2, 3] [1, 2, 3]。The simplifier then proves isPrefix [1, 2, 3] [1, 2, 3] by rewriting it to True.

也可以在定义之后的任何时间分配属性：One can also assign the attribute any time after the definition takes place:

在所有这些情况下，属性在导入声明所在文件的任何文件中都保持有效。添加 local 修饰符可以限制作用域（scope）：In all these cases, the attribute remains in effect in any file that imports the one in which the declaration occurs. Adding the local modifier restricts the scope:

另一个例子，我们可以使用 instance 命令将记号 ≤ 分配给 isPrefix 关系。该命令将在类型类（type classes）一章中解释，其工作原理是将 [instance] 属性分配给相关联的定义。For another example, we can use the instance command to assign the notation ≤ to the isPrefix relation. That command, which will be explained in the chapter on type classes, works by assigning an [instance] attribute to the associated definition.

该分配也可以设为局部（local）：That assignment can also be made local:

在下面的记号（Notation）中，我们将讨论 Lean 定义记号的机制，并看到它们也支持 local 修饰符。然而，在设置选项（Setting Options）中，我们将讨论 Lean 设置选项的机制，它不遵循此模式：选项只能局部设置，也就是说，它们的作用域总是限于当前章节或当前文件。In Notation below, we will discuss Lean's mechanisms for defining notation, and see that they also support the local modifier. However, in Setting Options, we will discuss Lean's mechanisms for setting options, which does not follow this pattern: options can only be set locally, which is to say, their scope is always restricted to the current section or current file.

6.6. 更多关于隐式参数（Implicit Arguments）6.6. More on Implicit Arguments🔗

在隐式参数（Implicit Arguments）中，我们看到如果 Lean 将项（term）t 的类型显示为 {x : α} → β x，那么花括号表示 x 已被标记为 t 的隐式参数（implicit argument）。这意味着每当你写 t 时，就会插入一个占位符，或“洞”，因此 t 被替换为 @t _。如果你不希望发生这种情况，则必须写 @t 代替。In Implicit Arguments, we saw that if Lean displays the type of a term t as {x : α} → β x, then the curly brackets indicate that x has been marked as an implicit argument to t. This means that whenever you write t, a placeholder, or “hole,” is inserted, so that t is replaced by @t _. If you don't want that to happen, you have to write @t instead.

注意，隐式参数是 eager 地插入的。假设我们定义一个函数 f : (x : Nat) → {y : Nat} → (z : Nat) → (z + y)。那么，当我们写下表达式 f 7 而没有进一步的参数时，它被解析为 @f 7 _。Notice that implicit arguments are inserted eagerly. Suppose we define a function f : (x : Nat) → {y : Nat} → (z : Nat) → Nat. Then, when we write the expression f 7 without further arguments, it is parsed as @f 7 _.

Lean 提供了一种较弱的注解，指定占位符只应在《在》随后的显式参数《之前》添加。它可以写成双花括号形式，因此 f 的类型将是 f : (x : Nat) → {{y : Nat}} → (z : Nat) → (z + y)。使用此注解，表达式 f 7 将被原样解析，而 f 7 3 将被解析为 @f 7 _ 3，与强注解一样。此注解也可以写为 ⦃y : Nat⦄，其中 Unicode 括号分别通过输入 \{{ 和 \}} 输入。Lean offers a weaker annotation which specifies that a placeholder should only be added before a subsequent explicit argument. It can be written with double braces, so the type of f would be f : (x : Nat) → {{y : Nat}} → (z : Nat) → Nat. With this annotation, the expression f 7 would be parsed as is, whereas f 7 3 would be parsed as @f 7 _ 3, just as it would be with the strong annotation. This annotation can also be written as ⦃y : Nat⦄, where the Unicode brackets are entered as \{{ and \}}, respectively.

为了说明区别，请考虑以下示例，该示例表明一个自反的欧几里得关系（euclidean relation）既是对称的（symmetric）也是传递的（transitive）。To illustrate the difference, consider the following example, which shows that a reflexive euclidean relation is both symmetric and transitive.

euclr : r ?m.3 ?m.4 → r ?m.3 ?m.5 → r ?m.4 ?m.5

结果被分解为小步骤：th1 表明自反且欧几里得的关系是对称的，th2 表明对称且欧几里得的关系是传递的。然后 th3 结合了这两个结果。但请注意，我们必须手动禁用 euclr 中的隐式参数，否则会插入过多的隐式参数。如果我们使用弱隐式参数，问题就会消失：The results are broken down into small steps: th1 shows that a relation that is reflexive and euclidean is symmetric, and th2 shows that a relation that is symmetric and euclidean is transitive. Then th3 combines the two results. But notice that we have to manually disable the implicit arguments in euclr, because otherwise too many implicit arguments are inserted. The problem goes away if we use weak implicit arguments:

euclr : Euclidean r

还有第三种隐式参数，用方括号 [ 和 ] 表示。它们用于类型类（type class），如类型类（type classes）一章所述。There is a third kind of implicit argument that is denoted with square brackets, [ and ]. These are used for type classes, as explained in the chapter on type classes.

6.7. 记号（Notation）6.7. Notation🔗

Lean 中的标识符可以包含任何字母数字字符，包括希腊字符（除了 ∀、Σ 和 λ，正如我们所见，它们在依值类型论中有特殊含义）。它们还可以包含下标，可以通过输入 \_ 后跟所需下标字符来输入。Identifiers in Lean can include any alphanumeric characters, including Greek characters (other than ∀ , Σ , and λ , which, as we have seen, have a special meaning in the dependent type theory). They can also include subscripts, which can be entered by typing \_ followed by the desired subscripted character.

Lean 的解析器（parser）是可扩展的，也就是说，我们可以定义新的记号。Lean's parser is extensible, which is to say, we can define new notation.

Lean 的语法可以在各个层次上由用户扩展和定制，从基本的“混合固定（mixfix）”记号到自定义的精化器（elaborator）。事实上，所有内置语法都使用与用户相同的机制和 API 进行解析和处理。在本节中，我们将描述和解释各种扩展点。Lean's syntax can be extended and customized by users at every level, ranging from basic “mixfix” notations to custom elaborators. In fact, all builtin syntax is parsed and processed using the same mechanisms and APIs open to users. In this section, we will describe and explain the various extension points.

虽然在编程语言中引入新记号是一个相对罕见的特性，有时甚至因可能混淆代码而受到批评，但在形式化（formalization）工作中，它是在代码中简洁地表达各自领域既有约定和记号的宝贵工具。超越基本记号，Lean 将常见样板代码分解为（行为良好的）宏以及嵌入整个自定义领域特定语言（DSL）以高效且可读地编码子问题的能力，对程序员和证明工程师都大有裨益。While introducing new notations is a relatively rare feature in programming languages and sometimes even frowned upon because of its potential to obscure code, it is an invaluable tool in formalization for expressing established conventions and notations of the respective field succinctly in code. Going beyond basic notations, Lean's ability to factor out common boilerplate code into (well-behaved) macros and to embed entire custom domain specific languages (DSLs) to textually encode subproblems efficiently and readably can be of great benefit to both programmers and proof engineers alike.

0

6.8. 强制类型转换（Coercions）6.8. Coercions🔗

在 Lean 中，自然数类型 Nat 与整数类型 Int 不同。但有一个函数 Int.ofNat 将自然数嵌入到整数中，这意味着在需要时我们可以将任何自然数视为整数。Lean 有检测和插入这种强制类型转换（coercion）的机制。可以使用重载的 ↑ 运算符显式请求强制类型转换。In Lean, the type of natural numbers, Nat, is different from the type of integers, Int. But there is a function Int.ofNat that embeds the natural numbers in the integers, meaning that we can view any natural number as an integer, when needed. Lean has mechanisms to detect and insert coercions of this sort. Coercions can be explicitly requested using the overloaded ↑ operator.

i + ↑m : Int

i + ↑m + j : Int

i + ↑m + ↑n : Int

6.9. 显示信息（Displaying Information）6.9. Displaying Information🔗

有多种方式可以向 Lean 查询关于其当前状态和当前上下文中可用的对象与定理的信息。你已经见过最常用的两种：#check 和 #eval。请记住，#check 通常与 @ 运算符一起使用，该运算符使定理或定义的所有参数变为显式。此外，你可以使用 #print 命令获取关于任何标识符的信息。如果标识符表示一个定义或定理，Lean 会打印该符号的类型及其定义。如果它是一个常量或公理（axiom），Lean 会指示这一事实并显示其类型。There are a number of ways in which you can query Lean for information about its current state and the objects and theorems that are available in the current context. You have already seen two of the most common ones, #check and #eval. Remember that #check is often used in conjunction with the @ operator, which makes all of the arguments to a theorem or definition explicit. In addition, you can use the #print command to get information about any identifier. If the identifier denotes a definition or theorem, Lean prints the type of the symbol, and its definition. If it is a constant or an axiom, Lean indicates that fact, and shows the type.

Eq.{u_1} {α : Sort u_1} : α → α → Prop

@Eq : {α : Sort u_1} → α → α → Prop

Eq.symm.{u} {α : Sort u} {a b : α} (h : a = b) : b = a

@Eq.symm : ∀ {α : Sort u_1} {a b : α}, a = b → b = a

theorem Eq.symm.{u} : ∀ {α : Sort u} {a b : α}, a = b → b = a :=
fun {α} {a b} h => h ▸ rfl

And (a b : Prop) : Prop

And.intro {a b : Prop} (left : a) (right : b) : a ∧ b

@And.intro : ∀ {a b : Prop}, a → b → a ∧ b

foo.{u} {α : Type u} (x : α) : α

@foo : {α : Type u_1} → α → α

def foo.{u} : {α : Type u} → α → α :=
fun {α} x => x

6.10. 设置选项（Setting Options）6.10. Setting Options🔗

Lean 维护许多可以由用户设置以控制其行为的内部变量（internal variable）。设置语法的格式如下：Lean maintains a number of internal variables that can be set by users to control its behavior. The syntax for doing so is as follows:

set_option <name> <value>set_option <name> <value>

一个非常有用的选项系列控制着 Lean 的美观打印机（pretty printer）显示项的方式。以下选项接受 true 或 false 作为输入：One very useful family of options controls the way Lean's pretty printer displays terms. The following options take an input of true or false:

pp.explicit  : display implicit arguments
pp.universes : display hidden universe parameters
pp.notation  : display output using defined notations

例如，以下设置会产生长得多的输出：As an example, the following settings yield much longer output:

@Eq.{1} Nat
  (@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat)
    (@OfNat.ofNat.{0} Nat (nat_lit 2) (instOfNatNat (nat_lit 2)))
    (@OfNat.ofNat.{0} Nat (nat_lit 2) (instOfNatNat (nat_lit 2))))
  (@OfNat.ofNat.{0} Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) : Prop

@Eq.{1} (Nat → Nat)
  (fun x =>
    @HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) x
      (@OfNat.ofNat.{0} Nat (nat_lit 2) (instOfNatNat (nat_lit 2))))
  fun x =>
  @HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) x
    (@OfNat.ofNat.{0} Nat (nat_lit 3) (instOfNatNat (nat_lit 3)))

(fun x =>
    @HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) x
      (@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))
  (@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1))) : Nat

命令 set_option pp.all true 一次性完成所有这些设置，而 set_option pp.all false 恢复到以前的值。当你调试证明或试图理解晦涩的错误消息时，打印额外信息通常非常有用。不过，信息过多可能令人不知所措，Lean 的默认设置通常足以应对常规交互。The command set_option pp.all true carries out these settings all at once, whereas set_option pp.all false reverts to the previous values. Pretty printing additional information is often very useful when you are debugging a proof, or trying to understand a cryptic error message. Too much information can be overwhelming, though, and Lean's defaults are generally sufficient for ordinary interactions.

6.11. 使用库（Using the Library）6.11. Using the Library🔗

要有效使用 Lean，你不可避免地需要使用库中的定义和定理。回想一下，文件开头的 import 命令会导入其他文件中先前编译的结果，且导入是传递的：如果导入 Foo，而 Foo 导入了 Bar，那么 Bar 中的定义和定理也对你可用了。但是，打开命名空间以提供较短名称的操作不会传递。在每个文件中，你需要打开希望使用的命名空间。To use Lean effectively you will inevitably need to make use of definitions and theorems in the library. Recall that the import command at the beginning of a file imports previously compiled results from other files, and that importing is transitive; if you import Foo and Foo imports Bar, then the definitions and theorems from Bar are available to you as well. But the act of opening a namespace, which provides shorter names, does not carry over. In each file, you need to open the namespaces you wish to use.

总的来说，熟悉库及其内容对你来说很重要，这样你才能知道有哪些定理、定义、记号和资源可供使用。下面我们将看到 Lean 的编辑器模式也可以帮助你找到需要的内容，但直接研究库的内容通常是不可避免的。Lean 的标准库可以在 GitHub 上在线找到：In general, it is important for you to be familiar with the library and its contents, so you know what theorems, definitions, notations, and resources are available to you. Below we will see that Lean's editor modes can also help you find things you need, but studying the contents of the library directly is often unavoidable. Lean's standard library can be found online, on GitHub:

• https://github.com/leanprover/lean4/tree/master/src/Inithttps://github.com/leanprover/lean4/tree/master/src/Init

• https://github.com/leanprover/lean4/tree/master/src/Stdhttps://github.com/leanprover/lean4/tree/master/src/Std

你可以使用 GitHub 的浏览器界面查看这些目录和文件的内容。如果你在本地计算机上安装了 Lean，可以在 lean 文件夹中找到该库，并使用文件管理器浏览。每个文件顶部的注释标题提供了附加信息。You can see the contents of these directories and files using GitHub's browser interface. If you have installed Lean on your own computer, you can find the library in the lean folder, and explore it with your file manager. Comment headers at the top of each file provide additional information.

Lean 库的开发人员遵循一般的命名指南，使得更容易猜测所需定理的名称，或使用支持此功能的 Lean 模式编辑器中的 Tab 补全来查找它，这将在下一节讨论。标识符通常是 camelCase，类型是 CamelCase。对于定理名称，我们依赖描述性名称，其中不同的组成部分由 _ 分隔。通常，定理的名称仅描述其结论：Lean's library developers follow general naming guidelines to make it easier to guess the name of a theorem you need, or to find it using tab completion in editors with a Lean mode that supports this, which is discussed in the next section. Identifiers are generally camelCase, and types are CamelCase. For theorem names, we rely on descriptive names where the different components are separated by _s. Often the name of theorem simply describes the conclusion:

Nat.succ_ne_zero (n : Nat) : n.succ ≠ 0

Nat.zero_add (n : Nat) : 0 + n = n

Nat.mul_one (n : Nat) : n * 1 = n

Nat.le_of_succ_le_succ {n m : Nat} : n.succ ≤ m.succ → n ≤ m

请记住，Lean 中的标识符可以组织成分层命名空间。例如，命名空间 Nat 中的定理 le_of_succ_le_succ 的全名是 Nat.le_of_succ_le_succ，但较短的名称可通过命令 open Nat 获得（对于未标记为 protected 的名称）。我们将在归纳类型（inductive types）和结构与记录（structures and records）章节中看到，在 Lean 中定义结构和归纳数据类型会生成相关的操作，这些操作存储在与所定义类型同名的命名空间中。例如，积类型（product type）带有以下操作：Remember that identifiers in Lean can be organized into hierarchical namespaces. For example, the theorem named le_of_succ_le_succ in the namespace Nat has full name Nat.le_of_succ_le_succ, but the shorter name is made available by the command open Nat (for names not marked as protected). We will see in the chapters on inductive types and structures and records that defining structures and inductive data types in Lean generates associated operations, and these are stored in a namespace with the same name as the type under definition. For example, the product type comes with the following operations:

@Prod.mk : {α : Type u_1} → {β : Type u_2} → α → β → α × β

@Prod.fst : {α : Type u_1} → {β : Type u_2} → α × β → α

@Prod.snd : {α : Type u_1} → {β : Type u_2} → α × β → β