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行を書かなくてもよくなります
- ExtractionでOCamlのコードを生成する場合にlistとpairはそれぞれOCamlのlistとpairに賢く対応するようになりました
- 有限集合に関するライブラリFSet, FMapあたりが大きく変わりました
- CoqIDEのデフォルトフォントが変わりました
- 最新のOCaml 3.11に対応しました
- etc...
早速ダウンロードしよう!
http://coq.inria.fr/distrib-eng.html