2014-11-19から1日間の記事一覧

Coq入門 - 2.1

coq

進捗ありません。 疑問メモ 矛盾を示すのが難しい forall n:nat, S n <= 0 と forall n:nat, S n > 0 があれば矛盾を示すのは簡単に見える けど、どうやるのかわからない forall n: nat, S n <= 0 はPropということでいいんだよな・・ CheckしてみるとPropと…