二週間くらいなにも書いてないので

一応生存を主張。
この間、論文を書いて、終わってへばって、次の論文に向けていろいろ考え中。
アイディアは大体固まったので、もう少し詰めてからやってみるかな、という感じ。
Coqのサブセットもその一つ。
まあ、Notationないけどね！
Typeもないけどね！！*1
とか大体そんなことを考えている。

*1:Typeは項ではない、特殊な型として用いるから「存在しない」わけじゃないが、Coqのように自由には使えない。sigが書けないのが若干気になるが・・・