1
数学的証明を形式的記述するための対象言語 (object language) に対して,証明戦略の記述用の言語であるメタ言語 (Meta Language) の頭文字をとった.
2
[1; 2; 3] という記法もある
3
ヘッダ部のopen宣言はトークン宣言部分では 有効ではないので,Syntax. をつけることが必要である.
4
この 区別はコンパイラの教科書で見られる左辺値(L-value),右 辺値(R-value)と関連する
5
これまで型変数は「何の型にでも置き換えてよい」ものとして説明してきたが, ここでの型変数は「特定の型を表す」記号であり,代数方程式における変数に近い. 「任意の型で置き換え可能」な型変数は次節で再登場する.
6
他にもいろいろな回避策が 考えられる.「計算と論理」の講義で関連した問題に詳しく触れられる(か もしれない).
7
関数などの仮引数の名前を使われている場所といっしょに 変えても同じ関数を表していることと同様の現象と考えられる.