23. 记法与宏🔗

不同的数学领域有各自的记法惯例，许多记法在不同领域中会以不同含义重复使用。形式化开发必须能够使用既有记法：形式化数学本就困难，而在不同语法之间转换所带来的心智负担可能相当沉重。与此同时，控制记法扩展的作用域也很重要。许多领域使用形式相近但含义迥异的记法；应当能够把这些不同领域的开发组合起来，同时让读者和系统都知道文件任一区域中采用的是哪套惯例。

Lean 使用多种机制解决记法可扩展性问题，每种机制负责问题的不同方面。它们可以灵活组合，以达到所需效果：

可扩展解析器 能以声明式方式实现种类繁多的记法惯例，并灵活地将它们组合起来。
宏可以轻松地把新语法映射到现有语法，这是为新构造赋予含义的一种简单方法。得益于卫生性和源位置的自动传播，这一过程不会干扰 Lean 的交互功能。
精译器在宏的表达能力不足时，为新语法提供与 Lean 自身语法所用相同的工具。
记法可同时定义解析器扩展、宏和美化打印器。定义中缀、前缀或后缀运算符时，自定义运算符会自动处理优先级与结合性。
底层解析器扩展能够以修改词法单元和空白规则的方式扩展解析器，甚至可以完全替换 Lean 的语法。这是一个需要熟悉 Lean 内部机制的高级主题；尽管如此，无需修改编译器便能做到这一点仍十分重要。本参考手册正是使用一种语言扩展编写的：它以类似 Markdown 的文档语言替换 Lean 的具体语法，但源文件仍然是 Lean 文件。