coq2scalaをさわってみたhttp://proofcafe.org/wiki/Coq2Scala を試してみました。 インストールはhgでソースコードとってきて、 ./configure make world make install でおｋ。 Extraction Language Scala. が使えちゃうCoqがインストールされます。 使ってみた とりあえず自然数と足し算を定義してみます。 吐き出されたScalaのコード。 Notationは無視される？ パラメータとらない場合はcase object使って欲しいかも・・・・ あとインデントも付くとうれしい。 ClassとInstanceを使ってみる Monoidを定義してみた。 私はtraitとimplicit parameterでかっこ良く変換されるのかな！？と期待。 結果は・・・・・ (´・ω・｀)ｼｮﾎﾞｰﾝ 明示的にインスタンスを渡して関数を得る感じ
