Chapter 06: Lean の仕組み

この章では，Lean を「証明を書くための言語」としてだけでなく， 「ソースコードを読み，エラボレートし，カーネルで検査し，ビルド成果物を作るシステム」として眺めます．

扱う内容は次の通りです．

• Lean の処理パイプライン
• カーネル，エラボレータ，抽象構文木
• .olean と .ilean
• VS Code を使わずに Lean と相互作用する方法
• プロジェクトのファイル構造と module

参考:

• Lean Language Reference: https://lean-lang.org/doc/reference/latest/
  • Elaboration and Compilation: https://lean-lang.org/doc/reference/latest/Elaboration-and-Compilation/
  • Interacting with Lean: https://lean-lang.org/doc/reference/latest/Interacting-with-Lean/
  • Source Files and Modules: https://lean-lang.org/doc/reference/latest/Source-Files-and-Modules/
  • Build Tools and Distribution: https://lean-lang.org/doc/reference/latest/Build-Tools-and-Distribution/

注意として，Lean Language Reference の latest は常に最新系列の Lean を説明しています． この原稿では，Lean project の作成や Lean version の指定方法は Chapter 05 にまとめ， この章では Lean がソースコードをどのように処理するかに焦点を当てます． 細かいコマンド出力やビルド成果物の名前は Lean のバージョンによって少し異なることがあります． この章では，概念は Reference に沿って説明し，実行例はこのプロジェクトの Lean 4.30.0 で確認できる形にしています．

import Mathlib

namespace Chapter06

open Lean