13. 条款🔗

Terms 是在 Lean 中编写数学和程序的主要手段。精化器将它们转换为 Lean 的最小核心语言，然后由内核检查并编译执行。术语语法为任意扩展；本章记录了 Lean 提供的开箱即用的术语语法。