このBaseモジュールをインストールすれば、写真の用なコードを書くことが出来る。 ダウンロード: http://sourceforge.jp/projects/coqbase/ 具体的には以下のことを定義した。 標準出力へ出力するprint, println関数 命令をつなげるセミコロン演算子 依存型を使った型安全なprintf関数 natからOCamlのint、stringからOCamlのstringへの相互変換関数 Coqでのbool、sumbool、list、option型をそのままOCamlの型として使うための連携