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