totem_3 https://blog.hatena.ne.jp/totem_3/ エンジニアですよ！ https://totem3.hatenablog.jp/ coq 進捗ありません。 疑問メモ 矛盾を示すのが難しい forall n:nat, S n <= 0 と forall n:nat, S n > 0 があれば矛盾を示すのは簡単に見える けど、どうやるのかわからない forall n: nat, S n <= 0 はPropということでいいんだよな・・ CheckしてみるとPropとなるからやはりPropのはずだ forall n : nat, S n > 0 : Prop と思ったけど、これはforall n:natが付いた時で、仮定に H : S n <= 0 とあるとこのS n <= 0はそういう型ということになのか 何かしらPropに対する操… 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Ftotem3.hatenablog.jp%2Fentry%2F2014%2F11%2F19%2F090141" title=" Coq入門 - 2.1 - エンジニアですよ！" class="embed-card embed-blogcard" scrolling="no" frameborder="0" style="display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;"></iframe> Hatena Blog https://hatena.blog 2014-11-19 09:01:41 rich https://totem3.hatenablog.jp/entry/2014/11/19/090141 1.0 100%