Lean 语言参考
本文档是 Lean 语言参考。
它旨在对 Lean 作出全面而精确的描述：这是一部供 Lean 用户查阅细节的参考书，而不是面向新用户的教程。
其他文档请参阅 Lean 文档总览。
本手册涵盖 Lean 版本 4.31.0。
Lean 是一个基于依值类型论的交互式定理证明器，设计目标是在前沿数学和软件验证中同时使用。 Lean 的核心类型论有足够的表达能力来刻画非常复杂的数学对象，同时又足够简单，从而允许独立实现并降低影响可靠性的错误风险。 核心类型论由一个极小的 kernel 实现；内核除检查证明项外不做其他事情。 这一核心理论和内核由高级自动化机制支撑，而这些自动化机制通过富有表达力的 tactic 语言实现。 每个 tactic 都产生一个核心类型论中的项，并由内核检查；因此 tactic 中的错误不会威胁 Lean 整体的可靠性。 同 Lean 的许多其他部分一样，tactic 语言可由用户扩展，因此可以逐步构造以满足特定形式化项目的需要。 Tactic 本身用 Lean 编写，定义后即可立即使用；无需重建证明器，也无需加载外部模块。
Lean 同时也是一门纯函数式编程语言，具有基于引用计数的运行时系统等特性，能够高效处理紧凑数组结构、多线程以及单子式 IO。
作为一门编程语言，Lean 主要用 Lean 自身实现，其中包括语言服务器、构建工具、elaborator 和 tactic 系统。
本书本身使用 Verso 编写；Verso 是一个用 Lean 编写的文档创作工具。
即使主要兴趣在于书写证明，熟悉 Lean 的编程特性也很有价值，因为 Lean 程序用于实现新的 tactic 和证明自动化。 因此，本参考手册不在 Lean 的两个方面之间划出界线，而是将它们合在一起描述，使二者能够相互阐明。