Pure

1. 空列はPureの項ではない。
2. 任意の識別子は項になる。
3. 型推論される。
4. 勝手な識別子の型は型変数 'a とされる。型総称な変数ということだろう。
5. 併置は適用演算のはず。
6. ラムダ抽象は %x. A 、ピリオドの直後の空白は必須。
7. η変換は自動で行う。
8. β変換も自動で行う。
9. op ==> は項で、型は prop=>prop=>prop
10. PROPは予約された特殊なキーワードで、式をprop型だと強制するらしい。
11. PROPは前置されるが、優先度（結合度）は低い。
12. 型定数はpropだけ、射定数は==>だけの体系らしい。
13. なぜか分からないが、==> はPROPで型を強制しないと使えないようだ。
14. ['a, 'b]=>'c は、'a => 'b => 'c の略記。便利は便利。
15. Pureで定義されているclassは型クラスじゃないみたいだ。なんだ、これ？（いやっ、やはり型クラスか？）
16. 型が定義されているかどうかは typ "型表現" で分かる。
17. default_sortでsortが出てくるが、ソートは意味不明。

名前の導入は

1. axiomatizationのシグネチャ部に書く。事前に名前の型が必要。
2. 組み込み型以外の型（の名前）が必要なら、typedeclで宣言する。この宣言は、その名前が型の定数名だとマークするだけ。型の実体が決まるわけではなく、構文的に認められる（登録される）だけ。
3. 総称的な名前（不定な型を持つ名前）なら、型定数なしに導入できる。例：eq, lessなど。そのときの型変数はパラメータ（圏論なら対象類を走る変数）となる。
4. definition "名前 == 項" でも名前を導入できる。
5. datatypeもprimrecはPureでは存在しない。帰納的定義をどうするか？
6. typedecl は型構成子を定義するので、型変数（構成子の型パラメータ）を使える。
7. class宣言はある。sortという言葉もある。型クラスは別物か？関係が謎。
8. Pureのレベルでソートという、おそらくは型の集合のような概念があり、classはソートとして登録されているようだ。
9. Pureでもlocaleは使えるのでモジュール化は出来る。

axiomatization
  E:: "'a ⇒ 'a ⇒ prop" (infix "##" 50)
  where refl: "a ## a"

↑はOK、次はダメ、ワカラン！

axiomatization
  E:: "'a ⇒ 'a ⇒ prop" (infix "##" 50)
  where refl: "E a a"

↓はOK

axiomatization
  E:: "['a,  'a] ⇒ prop" (infix "##" 50)
where
 symm: "E a b ≡ E b a"

↓でもOK

axiomatization
  E:: "['a,  'a] ⇒ prop" (infix "##" 50)
where
 symm: "a ##  b ≡  b ## a"

納得いかん。