マクロ展開とエラボレータ¶
エラボレーションとは，ユーザー向けの構文を，Lean のコア型理論の式へ変換する処理です． この処理は単純な翻訳ではありません． 次のような作業も行います．
- 省略された暗黙引数を補う．
- 型を推論する．
- 型クラスインスタンスを探索する．
- overloaded notation の意味を決める．
- tactic script を証明項へ変換する．
- 再帰定義や pattern matching をコア言語が扱える形に変換する．
そのため，エラボレータは Lean の使いやすさの大部分を担っています． 一方で，最終的にできた項はカーネルによって検査されます．
エラボレーションには大きく分けて command elaboration と term elaboration があります．
command elaboration は，def，theorem，#check，open などのトップレベル command を処理し，
必要に応じて環境を更新します．
term elaboration は，型注釈，定義の右辺，定理の証明項などを，期待される型の情報も使いながら Expr にします．
tactic の実行は term elaboration の特殊な場合と考えられ，最終的には証明項を構成します．
syntax "foo_demo_true" : term
macro_rules
| `(foo_demo_true) => `(True)
#check foo_demo_true
#check Lean.Macro
#check Lean.Elab.expandMacroImpl?
#check Lean.Elab.Command.CommandElabM
#check Lean.Elab.Command.elabCommandTopLevel
#check Lean.Elab.Term.TermElabM
#check Lean.Elab.Term.elabTerm
#check Lean.Elab.Tactic.TacticM
#check Lean.Meta.MetaM
foo_demo_true は，この章のために定義した小さな term macro です．
parser はまず foo_demo_true を Syntax として読みます．
その後，macro expansion によって True という構文に置き換えられ，term elaborator がそれを Prop の式として解釈します．
このように，macro は型のついた式を直接返すのではなく，構文を構文へ変換します．
CommandElabM，TermElabM，TacticM は，それぞれ command，term，tactic の elaborator が動くモナドです．
通常の証明を書く段階では意識しませんが，Lean で新しい command や tactic を作るときには，これらの世界でプログラムを書きます．
def fooDouble (n : Nat) : Nat :=
n + n
example : fooDouble 3 = 6 := by
rfl
#check fooDouble
#reduce fooDouble 3
#eval fooDouble 3
#check は型を表示します．
#reduce は，定義の展開や再帰子の計算規則など，Lean の definitional equality に関係する簡約で式を正規化します．
#eval はコンパイル・実行によって値を表示します．
証明では #check で名前の型を調べ，#reduce で定義の計算内容を確認し，#eval で実行可能なプログラムを試す，という使い分けをします．
#reduce と #eval はどちらも「計算結果」を見るコマンドですが，前者は証明で使われる簡約の見え方を確認するもの，
後者は実行可能なコードを実際に走らせるもの，と区別しておくとよいです．
set_option pp.all true を使うと，pretty printer が通常は隠している情報も多く表示します．
暗黙引数や universe，型クラス引数が見えるため，Lean がどれだけ多くの情報を補っているかを確認できます．