2007-06-25から1日間の記事一覧

1行でできるCoqプログラム

次の1行を書いて、〜.vというファイルを作ってみよう。 Extraction "plus.ml" plus. これであなたも立派なコカーだ!じゃあ早速コンパイルしてみよう。 /yoshihiro$ coqc 〜.v これで、plusという名前のCoqにもともと用意されている足し算関数がOCamlに変換…