IFOLとold appl syntax
IFOL上のセオリーだと、term "(%x. (%y. x)) a" がエラーになる。その理由は、
setup Pure_Thy.old_appl_syntax_setup
というコマンドが実行されており、これによって、Pureの併置による適用の構文がキャンセルされて、x(y) という形でないと適用とはみなされなくなる。
なんで旧式適用構文（old appl syntax）を使っているかは知らない。ちょっと迷惑だ。
このブログは、旧・はてなダイアリー「檜山正幸のキマイラ飼育記 メモ編」（http://d.hatena.ne.jp/m-hiyama-memo/）のデータを移行・保存したものであり、今後（2019年1月以降）更新の予定はありません。
今後の更新は、新しいブログ http://m-hiyama-memo.hatenablog.com/ で行います。
IFOL上のセオリーだと、term "(%x. (%y. x)) a" がエラーになる。その理由は、
setup Pure_Thy.old_appl_syntax_setup
というコマンドが実行されており、これによって、Pureの併置による適用の構文がキャンセルされて、x(y) という形でないと適用とはみなされなくなる。
なんで旧式適用構文（old appl syntax）を使っているかは知らない。ちょっと迷惑だ。