总结
求值与执行
副作用是程序执行中超出数学表达式求值范围的部分，例如读取文件、抛出异常或驱动工业机械。
虽然大多数语言允许在求值期间发生副作用，但 Lean 不会。相反，Lean 有一个名为 IO 的类型，
它表示使用副作用的程序的 描述（Description） 。然后由语言的运行时系统执行这些描述，
该系统会调用 Lean 表达式求值器来执行特定计算。类型为 IO α 的值称为 IO 活动 。
最简单的是 pure，它返回其参数并且没有实际副作用。
IO 操作还可以理解为将整个世界作为参数并返回一个副作用已经发生的全新世界的函数。在幕后，
IO 库确保世界永远不会被复制、创建或销毁。虽然这种副作用模型实际上无法实现，
因为整个宇宙太大而无法放入内存，但现实世界可以用一个在程序中传递的令牌来表示。
IO 活动 main 会在程序启动时执行。main 可拥有以下三种类型：
main : IO Unit用于无法读取其命令行参数且始终返回退出码0的简单程序，main : IO UInt32用于没有参数的程序，该程序可能会发出成功或失败信号，以及main : List String → IO UInt32用于获取命令行参数并发出成功或失败信号的程序。
do 记法
Lean 标准库提供了许多基本 IO 活动，表示诸如读写文件以及与标准输入和标准输出交互之类的作用。
这些基本 IO 活动使用 do 语法组合成更大的 IO 活动，
do 语法是用于编写具有副作用的程序描述的内置领域专用语言。
do 表达式包含一系列 语句（Statement） ，这些语句可以是：
- 表示
IO活动的表达式， - 使用
let和:=的普通局部定义，该定义的名称引用了所提供表达式的值，或者 - 使用
let和←的局部定义，该定义的名称引用了执行所提供表达式的结果值。
使用 do 编写的 IO 活动一次只执行一条语句。
此外，直接出现在 do 下面的 if 和 match 表达式隐式地被认为在每个分支中都有自己的 do。
在 do 表达式内部， 嵌套活动（Nested Action） 是括号下紧跟左箭头的表达式。
Lean 编译器会隐式地将它们提升到最近的封闭 do 中，该 do 可能隐式地是 match 或 if
表达式分支的一部分，并为它们提供一个唯一的名称。然后，此唯一名称将替换嵌套活动的原始位置。
编译并运行程序
一个由包含 main 定义的单个文件组成的 Lean 程序可以使用 lean --run FILE 运行。
虽然这可能是开始使用简单程序的好方法，但大多数程序最终都会升级为多文件项目，
在运行之前应该对其进行编译。
Lean 项目被组织成 包（Package） ，它们是库和可执行文件的集合，以及相关的依赖项和构建配置的信息。
包使用 Lean 构建工具 Lake 来描述。使用 lake new 可在新目录中创建一个 Lake 包，
或使用 lake init 在当前目录中创建一个包。Lake 包配置是另一种领域专用的语言。
可使用 lake build 构建项目。
偏函数
遵循表达式求值的数学模型的一个结果，就是每个表达式都必定有一个值。
这排除了不完全的模式匹配（即无法覆盖数据类型的全部构造子）和可能陷入无限循环的程序。
Lean 确保了所有 match 表达式会涵盖所有情况，并且所有递归函数要么是结构化递归的，
要么具有明确的停机证明。
然而，一些现实的程序需要编写无限循环的能力，因为它们需要处理潜在的无限数据，例如 POSIX 流。
Lean 提供了一个逃生舱：标记为 partial 的 偏函数（Partial Function） 定义不需要终止。
然而这是有代价的，由于类型是 Lean 语言的一等部分，所以函数可以返回类型。
然而，偏函数在类型检查期间不会被求值，因为函数中的无限循环可能会导致类型检查器进入死循环。
此外，数学证明无法检查偏函数的定义，这意味着使用它们的程序更难进行形式化证明。