本表继承旧中文手册术语并按当前项目规范维护。出现冲突时，以更具体的 Lean 语境条目为准。elaboration 固定译为“精译”，elaborator 固定译为“精译器”。新增或修改术语应在 PR 中说明。
| English | 中文 |
|---|---|
| ad-hoc | 特设（的） |
| alternative | 选取（的） |
| anti-symmetric | 反对称性 |
| arithmetic | 算术（的） |
| associative | 结合律 |
| binary operator | 二元运算符 |
| bisimulation | 互拟 |
| coalgebra | 逆代数 |
| codata type | 逆数据类型 |
| coinduction | 逆归纳 |
| commutative | 交换律 |
| composite type | 复合类型 |
| confluence | 合流性 |
| congruence | 合同性 |
| construct | 构造 |
| constructor | 构造子 |
| context | 上下文（必要时按语境译为“语境”） |
| copattern | 逆模式 |
| data constructor | 数据构造子 |
| de Bruijn | 名字不翻译 |
| dependent pair | 依值有序对 |
| dependent record | 依值记录体 |
| dependent type | 依值类型 |
| derivation | 演绎 |
| definitional equality | 定义等价 |
| defined constant | 已定义常量 |
| distribute | 分配律 |
| elaborate / elaboration | 精译 |
| elaborator | 精译器 |
| environment extensions | 环境扩展 |
| equational lemma | 等式引理 |
| evidence | 证据 |
| expression | 表达式 |
| extensionality | 外延性 |
| family of types | 类型族 |
| fixity declaration | 缀序声明 |
| function | 函数 |
| heterogeneous | 异质 |
| hole | 洞 |
| identity | 幺元 |
| identity function | 恒等函数 |
| idiom bracket | 习语括号 |
| implicit argument | 隐式参数 |
| impredicative | 非直谓的 |
| inductive type | 归纳类型 |
| info trees | 信息树 |
| initialization | 初始化 |
| interpreter | 解释器 |
| IO action | IO 操作 |
| kernel | 内核 |
| laziness | 惰性 |
| literal | 字面量 |
| measure | 度量 |
| metavariable | 元变量 |
| mutual block | 互递归块 |
| normal form | 规范形式 |
| opaque constant | 不透明常量 |
| operand | 操作数 |
| operator section | 操作符段 |
| parameterize | 参数化 |
| partial fixpoint | 偏不动点 |
| partial function | 偏函数 |
| pattern matching | 模式匹配 |
| predicative | 直谓的 |
| pre-definition | 预定义 |
| prelude | 前导库 |
| primitive type | 原语类型 |
| proof irrelevance | 证明无关性 |
| proposition | 命题 |
| propositional extensionality | 命题外延性 |
| qualifier | 限定式 |
| reasoning | 推理 |
| record | 记录体 |
| recursor | 递归子 |
| reduction | 规约 |
| reflection | 反射 |
| reflexive | 自反性 |
| row polymorphism | 行多态 |
| scope | 作用域 |
| section scope | 节作用域 |
| structure / struct | 结构体 |
| subsingleton | 子单元 |
| symmetric | 对称性 |
| term | 项 |
| total function | 全函数 |
| totality | 完全性 |
| transitive | 传递性 |
| type checker | 类型检查器 |
| type constructor | 类型构造子 |
| type inference | 类型推断 |
| unification | 合一 |
| universe | 宇宙 |
| universe level | 宇宙层级 |
| universe lifting | 宇宙提升 |
| universe parameter | 宇宙参数 |
| universe polymorphism | 宇宙多态 |
| vector | 向量 |
| well-founded recursion | 良基递归 |
| well-formed | 良构的 |
| well-typed | 良型的 |
.olean file |
.olean 文件 |
| η-equivalence | η-等价 |