概览

为了给读者一个清晰的路线图，这里首先介绍一下检查导出文件的完整过程，包括以下几个步骤：

• 解析导出文件：解析过程会产生若干基本种类的组件，包括名字（names）、宇宙层级（levels）与表达式（expressions），以及一系列的声明（declarations）。

• 解析得到的声明集合共同构成一个环境（environment）。环境是一个映射，将每个声明的名字对应到声明本身。这些声明正是类型检查过程真正的目标对象。

• 对环境中的每个声明，内核都会检查以下几点：

  1. 环境中尚未存在同名的声明；
  2. 声明中不存在重复的宇宙参数；
  3. 声明的类型必须确实是一个类型，而非一个值（即 infer declar.ty 的结果必须是 Sort <n> 形式的表达式）；
  4. 声明的类型中不包含任何自由变量（free variable）。

• 针对 定义（definitions）、定理（theorems） 和 不透明声明（opaque declarations），内核需要确保该定义值的推导类型（inferred type）与用户显式声明的类型是定义等价（definitionally equal）的。这一步是真正保证证明正确性的关键环节。特别地，对于定理而言，这对应于确认：“用户声称这是命题 P 的一个证明，内核实际检查该证明值是否构成了P的有效证明”。

• 对于 归纳类型声明（inductive declarations） 、它们的构造子（constructors）和递归子（recursors），内核会检查它们是否形式良好，并完全符合 Lean 类型理论的规则（稍后章节会详细展开）。

• 如果导出文件包含商类型（quotient types）的原始声明，那么内核也需确保这些声明具有正确的类型，并且 Eq 类型已存在且定义正确（因为商类型的定义依赖于相等关系）。

• 最后，通过美观打印器（pretty printer）输出用户所要求的声明，以便用户确认检查的声明是否与导出的声明相符。