Pure

Pureをいじっているが、性悪なシステムだな。

1. 接頭辞PROPの意味が分からない。他の構文とは違う、かなり特殊。
2. 型propには定数がなくて、true, falseもない。
3. PureとIFOLで関数適用の構文が違うのが非常にストレスだし、間違う。
4. prop型の定数はaxiomatizationで定義できるが、構文解析ではねられる。意味不明。Pureの構文解析がなんか特殊なのか？
5. op ==> を使うか、PROPを前置すれば大丈夫、気持ちワル。
6. Pureレベルでは、op ==> と中置==>は同値ではなくて、op ==> かPROP接頭辞を使わないと、Pure含意は書けない、ということか？ だとしたら極めて書きにくい。

isar-refの"8.4 The Pure syntax"を読むと分かるか？