Home > 一般 > Coq でよくあること

Coq でよくあること

  • 2014-01-23 (Thu) 01:39
  • 一般

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

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

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

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

閑話休題.

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

★下記に2つの英単語をスペースで区切って入力してください

Home > 一般 > Coq でよくあること

Search
Feeds

Page Top