まとめ

Lean の仕組みを理解するうえで，次の対応を押さえておくと見通しがよくなります．

• parser は文字列を Syntax にする．
• macro expansion は表面構文をより基本的な構文へ変換する．実際には elaboration と相互に入り組んで進む．
• elaborator は Syntax を型つきの Expr にし，暗黙引数，型クラス，tactic，再帰定義などを処理する．
• kernel は Expr がコア型理論の規則に従うかを検査する．
• .olean は検査済み環境を保存し，import を高速化する．
• このプロジェクトの Lean 4.30.0 では .ilean が language server のための索引として生成される．

普段の証明では，これらをすべて意識する必要はありません． しかし，エラーの原因を切り分けるとき，依存関係を管理するとき，AI や外部ツールから Lean を呼び出すときには，この構造を知っていることが役に立ちます．