---

1

数学的証明を形式的記述するための対象言語 (object language) に対して，証明戦略の記述用の言語であるメタ言語 (Meta Language) の頭文字をとった．

2

[1; 2; 3] という記法もある

5

これまで型変数は「何の型にでも置き換えてよい」ものとして説明してきたが， ここでの型変数は「特定の型を表す」記号であり，代数方程式における変数に近い． 「任意の型で置き換え可能」な型変数は次節で再登場する．

6

他にもいろいろな回避策が 考えられる．「計算と論理」の講義で関連した問題に詳しく触れられる(か もしれない)．

7

関数などの仮引数の名前を使われている場所といっしょに 変えても同じ関数を表していることと同様の現象と考えられる．