语法与宏🔗

在 Lean 中，代码首先被解析成语法，然后被精译成表达式。创建新的策略、命令和项，最简单的方式是在语法层面工作，把新语法映射到现有语法。变换语法的函数称为宏。

本章给出匹配、创建和变换语法的配方。

配方：

1. 准引用：创建与匹配语法
2. 编写一个宏
3. 添加语法（类别）