13. 项🔗

项是在 Lean 中书写数学和程序的主要手段。精译器将它们翻译为 Lean 的最小核心语言，随后由内核检查并编译执行。项的语法可以任意扩展；本章介绍 Lean 原生提供的项语法。