OCamlerのためのCoq便利モジュールを公開してみた


このBaseモジュールをインストールすれば、写真の用なコードを書くことが出来る。

ダウンロード: http://sourceforge.jp/projects/coqbase/

具体的には以下のことを定義した。

  • 標準出力へ出力するprint, println関数
  • 命令をつなげるセミコロン演算子
  • 依存型を使った型安全なprintf関数
  • natからOCamlのint、stringからOCamlのstringへの相互変換関数
  • Coqでのbool、sumbool、list、option型をそのままOCamlの型として使うための連携