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

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

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

5.1. 编码与表示 Encoding and Representation

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

Lean 的具体语法是可扩展的。 在像 Lean 这样的语言中， 想一次性完全描述语法是不可能的， 因为除了 新常量声明、 新归纳声明以外， 库还可能包含新的语法定义。 与其在此处完全描述语言，不如描述整体框架，然后 各个语言构造的具体语法会在对应章节中被详细介绍。

5.2.1. 空白 Whitespace

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

5.2.2. 注释 Comments

注释 Comments 是文件中那些被按照空白处理的部分， 尽管它们并非空白。注释有两种语法：

• 行内注释 Line Comments

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

• 区块注释 Block Comments

  一个不会作为词法单元出现且 没有被 - 尾随的 /- 将被用于开启区块注释。 区块注释会一直持续， 直至找到一个用于终止的 -/ 为止。 多个区块注释可以嵌套，并且只有当所有嵌套的区块注释都被终止后 -/ 才会终止最外层的区块注释。

/-- 和 /-! 开启的是文档注释而非普通注释。文档注释 同样也以 -/ 作为结束，并且 也可能包含嵌套的区块注释。 尽管文档注释看起来与普通注释很相似， 但是它们拥有自己的语法范畴； 他们的有效位置由 Lean 的语法所决定。

5.2.3. 关键字与标识符 Keywords and Identifiers

一个标识符 Identifier 包含一个或多个标识符组件。 多个标识符组件由 '.' 分隔。

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

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

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

那些包含一或多个 '.' 的标识符（意味着它们包含多个标识符组件） 被称为分层标识符 Hierarchical Identifiers。 分层标识符 既可用于表示导入名称， 也可用于表示命名空间中的名称。

5.3. 结构 Structure

module ::=
    header command*

5.3.1. 头部 Headers

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

header ::=
    module? -- 这个 module 是关键字
    import*

header ::= ...
  | module?
    prelude -- 这个 prelude 是关键字
    import*

如果 prelude 关键字存在， 那么便意味着该文件是 Lean 前导库 Prelude 的一部分， 前导库是那些无需显式导入就可以使用的代码—— 它不应该在 Lean 自身实现之外被使用。

prelude ::=
    prelude

import ::= ...
  | import ident

import ::= ...
  | public? meta? import all? ident

5.3.2. 命令 Commands

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

5.4. 模块与可见性 Modules and Visibility

模块是一个源文件，只不过其已主动选择 在公有信息和私有信息之间进行区分。 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

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

每个声明都有默认的可见性规则。一般来说， 所有名称默认都是私有的，除非是在公有区段中被声明的； 就连公有名称通常也会将声明的主体放置在私有作用域中， 即便是在暴露的定义中的证明也会保持私有。 每个声明命令的具体可见性规则都与声明本身一起记录。

索引 Index

术语

语法

常量

定理

公理

结构

选项

属性

例子