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

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

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

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

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