眠気と戦う日々

眠気と戦いながらいろいろと書くブログ

2014-08-05から1日間の記事一覧

内部でFixpointの関数を呼ぶ関数を定義した時にsimplだと証明できない

Coq

はい、表題のとおりです。 Coqを勉強していたらよくわからない挙動にぶつかったのでメモ。 問題のコード Fixpoint evenb (n:nat) : bool := match n with | O => true | S O => false | S (S n') => evenb n' end. Definition oddb (n:nat) : bool := negb (…