Home > Archives > 2014年01月23日

2014年01月23日

Coq でよくあること

vm_compute が爆速で驚く(インスタンスのサーチが速くなるのか?).

OCaml のバージョン違いでエラーを食らう(ハッシュテーブルのイテレーションの違いだかで omega の挙動が微妙に変わる).

tactics の知識不足でうまく証明が書けないから proof-term をダイレクトに書いてしまう.そしてそのせいで Code extraction に失敗する意味不明なエラーを食らって泣く.

まだまだ修行が足りない.

閑話休題.

svn のチェックアウトに数時間かかるってのはどうなんだろう? サーバが遠すぎるのが原因か?

Home > Archives > 2014年01月23日

Search
Feeds

Page Top