The Lean Reference Manual Release 3.3.0

• 语言: 英语
• 格式: .pdf
• 来源: leanprover.github.io

摘要

The Lean Reference Manual, Release 3.3.0, describes the lexical structure of the Lean language, including tokens, symbols, commands, and identifiers. Tokens are generated by the scanner using UTF-8 encoding and include symbols, commands, identifiers, strings, characters, numerals, decimals, quoted symbols, doc comments, and field notation. Symbols and commands are used in term notations and declarations. Identifiers consist of alphanumeric strings and may be hierarchical. The manual also covers universes, which are levels defining types, and expressions syntax, such as Sort u for universe level u, function types, application, and lambda expressions. Additionally, it discusses metaprogramming, including quotations and user-defined attributes.

AI总结

《The Lean Reference Manual Release 3.3.0》中文总结如下：

1. **简介**
Lean 是一个依赖类型的证明助手语言，本手册是其参考手册，详细描述了语言的核心特性和高级功能。

2. **词法结构（Lexical Structure）**
- **标记化（Tokenization）**：Lean 使用 UTF-8 编码进行标记化，标记包括符号、命令、标识符、字符串、字符、数值、引用的符号、文档评论等。
- **符号和命令**：符号用于项表示法，既可以是关键字，也可以是任意 Unicode 字符。命令用于引入顶级声明或操作，通常以关键字形式出现，部分命令以 `#` 开头。
- **标识符**：原子标识符是不以数字开头的字母数字字符串；层次标识符由多个原子标识符通过 `.` 分隔组成，部分可以通过 `«»` 元字符进行转义。
- **评论**：支持单行评论（`--`）和多行评论（`/-` 和 `-/`），多行评论可以嵌套。

3. **表达式（Expressions）**
- **宇宙（Universes）**：Lean 中的每种类型都属于某个宇宙级别（`Sort u`），宇宙级别可以是自然数、宇宙变量、表达式 `u + n`、`max u v` 或 `imax u v`。
- **表达式语法**：表达式包括宇宙 `Sort u`、常数 `c`、变量 `x`、函数类型 `Π x : α, β`、应用 `s t` 和 lambda 表达式 `λ x : α, t`。

4. **声明（Declarations）**
- **变量和宇宙**：`universe` 和 `universes` 命令用于引入宇宙变量，`variable` 和 `variables` 命令用于引入变量声明。变量可以通过 `#check` 命令检查类型，或者在定义或定理中自动声明。
- **隐式变量**：变量可以标记为隐式，用户可以通过 `include` 和 `omit` 命令手动管理变量的包含或排除。

5. **元编程（Metaprogramming）**
- Lean 提供代码引用和用户定义属性功能，支持高级元编程操作。

6. **库（Libraries）**
- Lean 提供标准库（Standard Library）、数学库（Mathematics Library）以及其他用户维护的库，用户也可以创建自定义库。

7. **包管理器（Package Manager）**
- Lean 支持通过 Git 和路径依赖管理外部库，例如使用 `mathlib` 库。

总结：本手册全面描述了 Lean 语言的核心特性、词法结构、表达式语法、声明机制、元编程能力和库管理功能，是 Lean 用户的重要参考资料。