# 翻译-Lean Language Reference-05-源文件与模块

{{< ctxset prefix="5" >}}
{{< labelindexset cnt_sect_digits="2" cnt_appr_digit="2" type="术语" >}}
{{< labelindexset cnt_sect_digits="2" cnt_appr_digit="2" type="语法" >}}
{{< labelindexset cnt_sect_digits="2" cnt_appr_digit="2" type="常量" >}}
{{< labelindexset cnt_sect_digits="2" cnt_appr_digit="2" type="定理" >}}
{{< labelindexset cnt_sect_digits="2" cnt_appr_digit="2" type="公理" >}}
{{< labelindexset cnt_sect_digits="2" cnt_appr_digit="2" type="归纳" >}}
{{< labelindexset cnt_sect_digits="2" cnt_appr_digit="2" type="结构" >}}
{{< labelindexset cnt_sect_digits="2" cnt_appr_digit="2" type="类型类" >}}
{{< labelindexset cnt_sect_digits="2" cnt_appr_digit="2" type="选项" >}}
{{< labelindexset cnt_sect_digits="2" cnt_appr_digit="2" type="属性" >}}
{{< labelindexset cnt_sect_digits="2" cnt_appr_digit="2" type="例子" cnt_sect_lv_max="2">}}

Lean 中最小的编译单元是单个源文件，
源文件可以通过文件名将其他源文件导入。换句话说，
文件名和文件夹结构在 Lean 代码中是有重要意义的。

每个源文件都有一个{{< labelindex 
  type="术语" 
  id_alias="源文件的导入名称"
  title_alias="源文件的导入名称 Import Name"
>}}
{{< /labelindex >}}**导入名称**，
导入名称由
  文件名和
  Lean 被启动的方式
所共同决定：
Lean 有一系列的{{< labelindex 
  type="术语" 
  id_alias="根目录"
  title_alias="根目录 Root Directory"
>}}
{{< /labelindex >}}**根目录**，
Lean 会在当中查找代码；而
源文件的导入名称则是文件名相对于根目录的路径，
文件名省略 `.lean` 后缀，
分隔符则是点号（`.`）而非斜杠（`/`）。
举个例子，如果 Lean 是以 `Projects/MyLib/src` 作为根目录启动的，
那么文件 `Projects/MyLib/src/Literature/Novel/SciFi.lean`
就可以通过 `Literature.Novel.SciFi` 来导入。

## 5.1. 编码与表示 Encoding and Representation {#S5-1}
{{< ctx level="2" >}}

Lean 的源文件内容都是 Unicode 文本文件，编码方式为 UTF-8。
源文件内的每一行都可以通过下述两种字符串结束：要么是
  单个换行符（
  `"\n"`，Unicode `'LINE FEED (LF)' (U+000A)`），要么便是
  单个换页符后跟单个换行符（
  `"\r\n"`，Unicode `'CARRIAGE RETURN (CR)' (U+000D)` 后跟 
  `'LINE FEED (LF)' (U+000A)`）。
即便如此，在解析或比较文件时 Lean 都会对行末进行规范处理，
因此所有文件在被比较时都会按照每行末尾为 `"\n"` 的情况进行分析。

## 5.2. 具体语法 Concrete Syntax {#S5-2}
{{< ctx level="2" >}}

Lean 的具体语法是可扩展的。
在像 Lean 这样的语言中，
想一次性完全描述语法是不可能的，
因为除了
  新常量声明、
  新[归纳声明]({{< relref "read-LeanRef-web-Chpt04.md" >}}#术语-归纳类型)以外，
  库还可能包含新的语法定义。
与其在此处完全描述语言，不如描述整体框架，然后
各个语言构造的具体语法会在对应章节中被详细介绍。

### 5.2.1. 空白 Whitespace {#S5-2-1}
{{< ctx level="3" >}}

Lean 中的词法单元可通过任意数目的{{< labelindex 
  type="术语" 
  id_alias="空白"
  title_alias="空白 Whitespace"
>}}
{{< /labelindex >}}**空白 Whitespace** 分隔。
空白可以是
  单个空格（`" "`，Unicode `'SPACE (SP)' (U+0020)`），或者是
  一个有效的换行符序列，或者是
  一个注释；
而
  制表符（Tab）、
  没有被新的行尾随的回车符（Carriage Return）
都不能算是有效的空白。

### 5.2.2. 注释 Comments {#S5-2-2}
{{< ctx level="3" >}}

{{< labelindex 
  type="术语" 
  id_alias="注释"
  title_alias="注释 Comments"
>}}
{{< /labelindex >}}**注释 Comments**
是文件中那些被按照空白处理的部分，
尽管它们并非空白。注释有两种语法：

- {{< labelindex 
  type="术语" 
  id_alias="行内注释"
  title_alias="行内注释 Line Comments"
>}}
{{< /labelindex >}}**行内注释 Line Comments**

  一个不会作为词法单元出现的 `--`
  将被用于开启行内注释。
  从初始的 `-` 开始算起到换行符为止的所有字符
  都会被视作是空白。

- {{< labelindex 
  type="术语" 
  id_alias="区块注释"
  title_alias="区块注释 Block Comments"
>}}
{{< /labelindex >}}**区块注释 Block Comments**

  一个不会作为词法单元出现且
  没有被 `-` 尾随的 `/-`
  将被用于开启区块注释。
  区块注释会一直持续，
  直至找到一个用于终止的 `-/` 为止。
  多个区块注释可以嵌套，并且只有当所有嵌套的区块注释都被终止后
  `-/` 才会终止最外层的区块注释。
  
`/--` 和 `/-!` 开启的是文档注释而非普通注释。文档注释
  同样也以 `-/` 作为结束，并且
  也可能包含嵌套的区块注释。
尽管文档注释看起来与普通注释很相似，
但是它们拥有自己的语法范畴；
他们的有效位置由 Lean 的语法所决定。

### 5.2.3. 关键字与标识符 Keywords and Identifiers {#S5-2-3}
{{< ctx level="3" >}}

一个{{< labelindex 
  type="术语" 
  id_alias="标识符"
  title_alias="标识符 Identifier"
>}}
{{< /labelindex >}}**标识符 Identifier** 包含一个或多个标识符组件。
多个标识符组件由 `'.'` 分隔。

标识符组件包含
  一个（类似）字母的字符或者是
  一个下划线（`'_'`），
然后尾随零或多个标识符后续字符。其中
字母字符可以是
  （大、小写）英文字母，而
类似字母的字符
  包含一系列非英语字母的字母脚本，包括
    在 Lean 中广泛使用的希腊字母脚本、
    科普特字母以及
    Unicode 字母符号块中的成员；后者如
      Mathematical Double-Struck 中的字符（包括 `ℕ` 和 `ℤ`）和缩写、
      Latin-1 Supplement 中的字母（除去 `×` 和 `÷`）以及
      Latin Extended-A 中的字母。
标识符后续字符可以是
  字母字符、
  类似字母的字符、
  下划线（`'_'`）、
  感叹号（`!`）、
  问号（`?`）、
  下标以及
  单引号（`'`）。
另外下划线在单独出现时并不构成一个有效的标识符。

标识符的组件也可以被一对法语引号（`'«'` 和 `'»'`）所包围。
这样的标识符组件可以包含除 `'»'` 之外的任意字符，
甚至连 `'«'`、`'.'` 和换行符都可以。
引号本身不属于标识符组件的一部分，因此 
`«x»` 和 `x` 表示同一个标识符。然而，
`«Nat.add»` 是一个单一组件的标识符，而 `Nat.add` 则拥有两个组件。

某些潜在的标识符组件可能是保留关键字。
具体的保留关键字集合取决于当前被激活的语法扩展集合，而后者又取决于
  已导入的文件集合以及
  已开启的命名空间集合；
因此想要为整个 Lean 语言枚举保留关键字是不可能的。
在大多数语法语境中，这些关键字要想作为标识符组件使用就必须包裹在法语引号内。
那些允许关键字在不使用法语引号的情况下作为标识符使用的语境——比如归纳类型中的构造函数名称，
则被称作是{{< labelindex 
  type="术语" 
  id_alias="原始标识符"
  title_alias="原始标识符 Raw Identifier"
>}}
{{< /labelindex >}}**原始标识符 Raw Identifier** 语境。

那些包含一或多个 `'.'` 的标识符（意味着它们包含多个标识符组件）
被称为{{< labelindex 
  type="术语" 
  id_alias="分层标识符"
  title_alias="分层标识符 Hierarchical Identifier"
>}}
{{< /labelindex >}}**分层标识符 Hierarchical Identifiers**。
分层标识符
  既可用于表示导入名称，
  也可用于表示命名空间中的名称。

## 5.3. 结构 Structure {#S5-3}
{{< ctx level="2" >}}

{{< labelindex 
  type="语法" 
  id_alias="源文件"
>}}
{{< /labelindex >}}
> [!info] 语法：{{< indexprint >}}
> 
> ```lean {wrapper=false, lineNos=false}
> module ::=
>     header command*
> ```
> 
> 源文件以一个{{< labelindex 
  type="术语" 
  id_alias="源文件头部"
  title_alias="源文件头部 File Header"
>}}
{{< /labelindex >}}**文件头部 File Header**开启，后面跟随一系列{{< labelindex 
  type="术语" 
  id_alias="命令"
  title_alias="命令 Command"
>}}
{{< /labelindex >}}**命令 Command**


### 5.3.1. 头部 Headers {#S5-3-1}
{{< ctx level="3" >}}

模块的头部列出了那些在当前模块之前应该被阐述的模块。
他们包含的声明在当前模块中将会是可见的。

{{< labelindex 
  type="语法" 
  id_alias="模块头部"
>}}
`module? …`
`module? prelude …`
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
模块头部包含一个可选关键字 `module`，
然后尾随一系列的 `import` 语句：

```lean {wrapper=false, lineNos=false}
header ::=
    module? -- 这个 module 是关键字
    import*
```

可选关键字 `prelude` 只能在 Lean 自己的源代码中使用：

```lean {wrapper=false, lineNos=false}
header ::= ...
  | module?
    prelude -- 这个 prelude 是关键字
    import*
```
{{< /admonition >}}

如果 `prelude` 关键字存在，
那么便意味着该文件是 Lean {{< labelindex 
  type="术语" 
  id_alias="前导库"
  title_alias="前导库 Prelude"
>}}
{{< /labelindex >}}**前导库 Prelude** 的一部分，
前导库是那些无需显式导入就可以使用的代码——
它不应该在 Lean 自身实现之外被使用。

{{< labelindex 
  type="语法" 
  id_alias="前导库模块"
>}}
`prelude`
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
```lean {wrapper=false, lineNos=false}
prelude ::=
    prelude
```
{{< /admonition >}}

{{< labelindex 
  type="语法" 
  id_alias="导入"
>}}
`import …`\
`public? meta? import all? …`
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
所有源文件都可以通过普通导入语法被导入：

```lean {wrapper=false, lineNos=false}
import ::= ...
  | import ident
```

在那些非模块的源文件中，这可以导入指定的 Lean 文件。
导入一个文件会使
  其内容以及
  其自身所导入的源文件的内容
在当前源文件中都变得可用，

源文件名称不一定非得与命名空间相对应。
源文件可以向任意命名空间添加名称，并且
导入一个源文件不会对当前的已开启的命名空间集合产生任何影响。

源文件的[导入名称](#术语-导入名称)会被转换为文件名，方法是
  将其名称中的点号（`'.'`）替换为目录分隔符，并
  在末尾添加 `.lean` 或 `.olean`。
Lean 会在其包含路径中搜索
  相应的中间构建产物或
  可导入的模块文件。

模块则可以使用下述语法导入：

```lean {wrapper=false, lineNos=false}
import ::= ...
  | public? meta? import all? ident
```

被模块导入的东西自己也必须是模块。在没有修饰符的情况下，
被导入的模块的公有作用域会被添加到当前模块的私有作用域中。
被当前模块导入的模块不会被进一步提供给那些导入当前模块的模块。
各个修饰符的意义如下：

- `public`

  被当前模块导入的模块的公有作用域
    会被添加到当前模块的公有作用域中，并且
    会被进一步提供给那些导入当前模块的模块。

- `meta`

  被当前模块导入的模块的内容
    会在当前模块的[元阶段 Meta Phase](https://lean-lang.org/doc/reference/latest/Source-Files-and-Modules/#--tech-term-meta-phase) 中变得可用。

- `all`

  被当前模块导入的模块的私有作用域
    会被添加到当前模块的私有作用域中。
{{< /admonition >}}

### 5.3.2. 命令 Commands {#S5-3-2}
{{< ctx level="3" >}}

[命令](#术语-命令) 是 Lean 中的顶层语句。
命令可以是
  归纳类型声明、
  定理、
  函数常量声明，或者是
  形如 `open` 或 `variable` 这样的命名空间修饰符，或者是
  形如 `#check` 这样的交互式查询。
命令的语法可由用户扩展，
命令甚至还可以[添加新的语法以用于解析后续命令](https://lean-lang.org/doc/reference/latest/Notations-and-Macros/#language-extension)。
具体的 Lean 命令不会在这里全部列出，
而是会在本手册的相应章节中进行详细介绍。

## 5.4. 模块与可见性 Modules and Visibility {#S5-4}
{{< ctx level="2" >}}

模块是一个源文件，只不过其已主动选择
在公有信息和私有信息之间进行区分。
Lean 会确保私有信息的修改不会影响到
仅导入其公有信息的下游客户端。
这种约束的好处有：

- **大幅缩短平均构建时间 Much-Improved Average Build Times**

  如果对文件做出的修改只会影响非导出信息（例如证明、注释和文档字符串），
  那么就不会触发在这些文件外部的重新构建。即便依赖文件必须被重新构建，
  那些不会被影响（由其 `import` 注解所决定）的文件也会被跳过。

- **掌控 API 的演变 Control Over API Evolution**

  库的作者可以确信：对非导出信息的修改不会影响到自己的库的下游用户。
  只要一个函数的签名被暴露，下游用户就无法依赖于任何涉及到该函数展开的定义等价性。
  这意味着库作者可以随心所欲地接纳更高效的算法，无需操心不小心破坏客户端代码的情况。

- **避免意外展开 Avoiding Accidental Unfolding**

  对定义可被展开的作用域进行限制既可以避免
    那些应该被更具体的定理所替代的归约，也可以避免
    那些实际上并非必要的无效归约。
  这提高了证明被阐述的速度。

- **更小的可执行文件 Smaller Executables**

  将编译期代码和运行时代码分离
  可以让 Lean 对死代码进行更积极的消除，
  从而确保诸如策略这样的元程序不会进入最终的二进制文件。

- **降低内存占用 Reduced Memory Usage**

  在进行导入时排除掉诸如证明之类的私有信息
  可以同时提高 Lean 在构建和编辑项目时的内存使用效率。
  将 mathlib4 移植到模块系统中的实践表明：
  在进一步最小化导入之前就可以节省将近 50% 的内存。

模块包含两个独立的作用域：
  公有作用域包含那些在导入模块时可见的信息，而
  私有作用域则包含那些通常只在模块内部可见的信息。
一些可以是私有或公有的信息的例子包括：

- **名称 Names**

  常量（如由 `def` 声明的常量、归纳类型构造子、归纳项构造子等）
  可以是私有的或者是公有的。公有常量的类型只能引用公有名称。

- **声明 Definitions**

  一个公有声明可以被暴露，也可以不被暴露。如果一个公有声明没有被暴露，
  那么它就无法在仅能访问公有作用域的语境中被展开。相反，
  客户端必须依赖于公有作用域中提供的关于该声明的定理。

每个声明都有默认的可见性规则。一般来说，
所有名称默认都是私有的，除非是在[公有区段]({{< relref "read-LeanRef-web-Chpt06.md" >}}#术语-公有区段)中被声明的；
就连公有名称通常也会将声明的主体放置在私有作用域中，
即便是在暴露的定义中的证明也会保持私有。
每个声明命令的具体可见性规则都与声明本身一起记录。

## 索引 Index {#index}

### 术语

{{< indexlist type="术语" sort="title" >}}

### 语法

{{< indexlist type="语法" >}}

### 常量

{{< indexlist type="常量" code_wrap=true >}}

### 定理

{{< indexlist type="定理" code_wrap=true >}}

### 公理

{{< indexlist type="公理" code_wrap=true >}}

### 结构

{{< indexlist type="结构" code_wrap=true >}}

### 选项

{{< indexlist type="选项" code_wrap=true >}}

### 属性

{{< indexlist type="属性" code_wrap=true >}}

### 例子

{{< indexlist type="例子" print_section=false >}}


---

> 作者: [沉积岩](ych817.github.io)  
> URL: https://ych817.github.io/posts/616d58b/