前回のつづき。POPL08チュートリアルのうちの基礎部分CoqIntro.vをやってみる。 http://www.cis.upenn.edu/~plclub/popl08-tutorial/code/coqdoc/CoqIntro.html CoqIntroはboolとnatからなる式言語を定義しているが、それが興味深い表現になっている。 言語…