2014年01月23日
Coq でよくあること
- 2014-01-23 (Thu)
- 一般
vm_compute が爆速で驚く(インスタンスのサーチが速くなるのか?).
OCaml のバージョン違いでエラーを食らう(ハッシュテーブルのイテレーションの違いだかで omega の挙動が微妙に変わる).
tactics の知識不足でうまく証明が書けないから proof-term をダイレクトに書いてしまう.そしてそのせいで Code extraction に失敗する意味不明なエラーを食らって泣く.
まだまだ修行が足りない.
閑話休題.
svn のチェックアウトに数時間かかるってのはどうなんだろう? サーバが遠すぎるのが原因か?
- Comments: 0
- TrackBack (Close): -