代码、语法与表达式
贡献者：subfish-zhou
代码的内部表示
Syntax 和 Expr 都是 Lean 核心库中定义的类型，在元编程中被广泛使用。Lean 为操作 Syntax 和 Expr 提供了丰富的 API。
语法
Lean 中的语法是可扩展的，能够表示各种各样的语法结构，包括变量、常量、函数应用、λ 抽象等等。把字符串转换为语法由解析器（Parser）完成，解析器是接受字符串作为输入、产生语法作为输出的函数。
操作语法由宏（Macro）完成，宏是接受语法作为输入、产生语法作为输出的函数。宏用于定义新的语法结构，以及对现有语法进行变换。
表达式
语法会进一步由精译器（elaborator）处理，精译器接受语法作为输入，产生表达式作为输出。精译（elaboration）过程进行类型推断、名字解析，以及其他变换，从而产生类型正确的表达式。
Lean 中的表达式由 Expr 类型表示，它是一种递归数据结构，能够表示各种各样的表达式，包括变量、常量、函数应用、λ 抽象等等。更复杂的元编程往往直接操作表达式，本书大多数配方都在这一层。