14. 記法とマクロ（Notations and Macros）🔗

数学では分野ごとに固有の記法の慣習を持っており、多くの記法が複数の分野で異なる意味として再利用されています。形式化の開発では確立された記法を使えることが重要です：数学の形式化はすでに難しいものになっており、構文間の変換による精神的オーバーヘッドは相当なものになります。同時に、記法の拡張範囲をコントロールできることも重要です。多くの分野では、全く異なる意味を持つ似た表記が使われており、読者とシステムの両方が、ファイルの任意の領域でどの記法が有効であるかを知ることができるような方法でこれらの別々の分野からの開発を組み合わせることが可能でなければならない。

Lean はさまざまなメカニズムで記法の拡張性の問題に取り組んでおり、それぞれが問題の異なる側面を解決しています。必要な結果を得るために、それらを柔軟に組み合わせることができます：

拡張可能なパーサ は非常に多様な記法規則を宣言的に実装し、柔軟に組み合わせることができます。
マクロにより、新しい構成に意味を与えるシンプルな方法によって新しい構文を既存の構文に簡単にマッピングすることができます。 hygiene とソース位置の自動伝播によって、このプロセスは Lean の対話的機能を妨げません。
エラボレータはマクロの表現力が不十分な場合に Lean 独自の構文と同じツールを使って新しい構文を提供します。
記法はパーサ拡張・マクロ・プリティプリンタを同時に定義できます。中置・前置・後置演算子を定義する場合、カスタム演算子が自動的に優先順位と結合性を考慮します。
低レベルのパーサ拡張は、トークンや空白に対するルールを変更したり、Lean の構文を完全に置き換えたりするような方法でパーサを拡張することを可能にします。これは高度なトピックであり、Lean の内部構造に精通している必要があります；とはいえ、コンパイラを修正することなくこれを行える可能性があることは重要です。このリファレンスマニュアルは Lean の具体的な構文を Markdown のような言語で置き換えた言語拡張を使って書かれていますが、ソースファイルは Lean のままです。