2012-05-25から1日間の記事一覧
久しぶりに Coq を触ったら, 昔書いた Coq のソースプログラムが通らなくなっていました. いろいろ原因を探ってみたところ, Coq 8.2 と Coq 8.3 で, 証明の開始時点での goal の形式が変わったためのようです. たとえば,Theorem eq_diff_0 (n m: nat) …
久しぶりに Coq を触ったら, 昔書いた Coq のソースプログラムが通らなくなっていました. いろいろ原因を探ってみたところ, Coq 8.2 と Coq 8.3 で, 証明の開始時点での goal の形式が変わったためのようです. たとえば,Theorem eq_diff_0 (n m: nat) …