読者です 読者をやめる 読者になる 読者になる

にわとり小屋でのプログラミング ブログ

名古屋のCoqエンジニアです。日記は勘で書いてるところがあるので細かいとこが違うことがあります。

Coq 8.2 リリース!

Coqがversion 8.1から8.2にバージョンアップしました。変更点は以下のいろいろ。

  • Haskellのような type class system が導入されました
  • coqcでコンパイル後のvoファイル を扱うcoqchkというツールが追加されました
  • Setoidのための書き換えタクティック setoid_rewrite が追加されました。
  • 再帰関数をFixpointで定義するときに、停止性を担保する引数を {struct hoge}のように書かなくてもよくなりました(もちろん書いてもよいです)
  • Agdaのような "forall {A}, P" という構文sugerが導入されました。"Implicit Arguments t [A]." という1行を書かなくてもよくなります
  • ExtractionOCamlのコードを生成する場合にlistとpairはそれぞれOCamlのlistとpairに賢く対応するようになりました
  • 有限集合に関するライブラリFSet, FMapあたりが大きく変わりました
  • CoqIDEのデフォルトフォントが変わりました
  • 最新のOCaml 3.11に対応しました
  • etc...

早速ダウンロードしよう!
http://coq.inria.fr/distrib-eng.html