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

今年もアンビグラムというほどのものではありませんが， それに近いものを作成してみました． これまでのもの ( 2008年 / 2009年 / 2010年 ) に比べるとわかりやすすぎますね． 昨年は全く更新しないという体たらくでしたが， 今年はこれで少なくとも一回は…