4. Type 系统
Terms，也称为 expressions，是 Lean 核心语言中意义的基本单位。 它们是由 精化器 根据用户编写的语法生成的。 Lean 的类型系统将术语与其类型相关联，这些类型本身也是术语。 类型可以被认为表示集合，而术语表示这些集合的各个元素。 如果项具有符合 Lean 的 类型论 规则的类型，则该项是 well-typed。 只有类型正确的术语才有意义。
术语是依值类型的 λ 演算：它们包括函数抽象、应用程序、变量和 let 绑定。
除了绑定变量之外，术语语言中的变量还可以指 构造函数、类型构造函数、递归函数、定义的常量 或不透明常量。
构造函数、类型构造函数、递归器和不透明常量不能进行替换，而定义的常量可以用它们的定义替换。
derivation 通过明确指示所使用的精确推理规则来演示术语的类型正确性。 隐含地，类型良好的术语可以代替证明其类型良好的推导。 Lean 的 类型论 足够明确，可以从类型良好的术语重建推导，这大大减少了存储完整推导所产生的开销，同时仍然具有足够的表现力来表示现代研究数学。 这意味着证明项是定理真实性的充分证据，并且可以进行独立验证。
除了具有类型之外，术语还通过 定义等价相关。 这是一种可机械检查的关系，在语法上将术语对其计算行为取模。 定义等价 包括 reduction 的以下形式：
- β（测试版）
通过替换绑定变量将函数抽象应用于参数
- δ（增量）
将出现的 已定义常量 替换为定义的值
- ι (iota)
减少目标是构造函数的递归器（原始递归）
- z (zeta)
用其定义值替换 let 绑定变量
- 商数减少
商类型函数提升运算符的归约应用于商的元素时
已进行所有可能减少的项采用 正常形式。
定义等价 包括函数 η-等价 和单构造函数归纳类型。
也就是说，如果 S 是具有字段 f1 和 f2 的结构，则 fun x => f x 定义上等于 f，S.mk x.f1 x.f2 定义上等于 x。
它还具有 证明无关性：同一命题的任何两个证明在定义上都是相等的。
它是自反且对称的，但不具有传递性。
定义等价 通过转换使用：如果两个术语在定义上相等，并且给定术语将其中之一作为其类型，则它也将另一个作为其类型。 由于 定义等价 包含约简，因此类型可以通过数据计算得出。
Computing types
当传递自然数时，函数 LengthList 计算一个与列表相对应的类型，其中包含恰好那么多的条目：
def LengthList (α : Type u) : Nat → Type u
| 0 => PUnit
| n + 1 => α × LengthList α n
由于 Lean 的元组嵌套在右侧，因此不需要多个嵌套括号：
example : LengthList Int 0 := ()
example : LengthList String 2 :=
("Hello", "there", ())
如果长度与条目数不匹配，则计算类型将与该术语不匹配：
example : LengthList String 5 :=
("Wrong", "number", ())
Lean 中的基本类型为 universes、function 类型、Quot 的商、归纳类型 的 类型构造函数。
定义的常量、递归器的应用、函数应用、公理或 不透明常量 还可以给出类型，就像它们可以产生任何其他类型的项一样。