23. 符号和宏🔗

不同的数学领域有自己的符号约定，并且许多符号在不同领域中以不同的含义重复使用。重要的是，形式化开发能够使用既定的符号：形式化数学已经很困难，并且语法之间翻译的心理开销可能很大。同时，能够控制符号扩展的范围也很重要。许多领域使用具有不同含义的相关符号，并且应该可以将这些单独领域的发展结合起来，使读者和系统都知道在文件的任何给定区域中哪个约定有效。

Lean 通过多种机制解决符号可扩展性问题，每种机制解决问题的不同方面。它们可以灵活组合以达到必要的结果：

extensible parser 允许以声明方式实现多种符号约定，并灵活组合。
宏允许将新语法轻松映射到现有语法，这是为新构造提供含义的简单方法。由于卫生和源位置的自动传播，此过程不会干扰 Lean 的交互功能。
Elaborators 提供新语法，在宏表达能力不足的情况下，可使用与 Lean 自己的语法相同的工具。
符号允许同时定义解析器扩展、宏和漂亮的打印机。定义中缀、前缀或后缀运算符时，自定义运算符自动处理优先级和关联性。
低级解析器扩展允许解析器以修改其标记和空格规则的方式进行扩展，甚至完全替换 Lean 的语法。这是一个高级主题，需要熟悉 Lean 内部结构；尽管如此，在不修改编译器的情况下完成此操作的可能性很重要。本参考手册是使用语言扩展编写的，该语言扩展用类似 Markdown 的语言来替换 Lean 的具体语法来编写文档，但源文件仍然是 Lean 文件。