一昨日（表示は昨日になるかもしれない）、Coqのサブセットを作ろうかな、と書いた。 でもサブセットってどのくらいよ？という問題が出てくる。 少し考えてみよう。 まず、Coqのサポートしている範囲を挙げる。 言語について：Vernacular（コマンド用言語、…

終わったら書こうと少し考えていたのだが、忘れて翌日になってしまった。 論文を書かないですごすという暴挙に出ているので、あまりまじめなネタが書けない（ここに書くくらいなら論文に書け、と）。 まあそういう冗談（？）はさておき、少しこのブログでや…