精译（elaboration）：扩展语法
贡献者：subfish-zhou
扩展 Lean 语法最简单的方式是编写宏，把新语法转换为已有语法（见 语法与宏）。不过，还有一种更强大的扩展方式：编写新的精译器（elaborator），把新语法转换成表达式。本章给出为项和命令的新语法编写精译器的配方。
配方：
扩展 Lean 语法最简单的方式是编写宏，把新语法转换为已有语法（见 语法与宏）。不过，还有一种更强大的扩展方式：编写新的精译器（elaborator），把新语法转换成表达式。本章给出为项和命令的新语法编写精译器的配方。
配方：