The Lean Reference Manual Release 3.3.0

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

摘要

The document provides a comprehensive reference manual for Lean 3.3.0, detailing its usage across various editors like VSCode and Emacs, package management, lexical structure, expressions, and declarations. It covers essential commands, tactics, and configurations, offering guidance on setting up projects and integrating Lean with different development environments.

AI总结

《The Lean Reference Manual Release 3.3.0》是一份关于Lean编程语言或证明助手的参考手册，主要内容如下：

1. **使用Lean**
- 提供了在不同环境中使用Lean的方法，包括在线、VSCode和Emacs。
- 介绍了如何使用包管理器（`leanpkg`）创建新包、添加依赖以及管理项目。

2. **词法结构**
- 定义了Lean的词法元素，包括符号、标识符、字符串字面量、字符字面量、数字字面量、引号符号等。
- 介绍了文档注释和字段符号的使用。

3. **表达式**
- 介绍了Lean中的表达式语法，包括宇宙、隐式参数、基本数据类型、构造器和匹配。
- 讨论了结构化证明、计算（包括β-归约、ζ-归约、δ-归约和ι-归约）以及公理的概念。

4. **声明**
- 描述了如何在Lean中进行声明，包括上下文、类型类、结构和记录等。
- 介绍了归纳类型、归纳族、相互和嵌套归纳定义，以及方程编译器的使用。

5. **其他命令**
- 包含了与宇宙和变量相关的命令。

手册内容详细且结构清晰，适合开发者和证明助手的用户参考。