Why3 をライブラリとして使う OCamlのコードのサンプル
-
opam install . --deps-onlyでパッケージをインストール -
why3 config detectを実行して Coq を認識させる -
dune buildでビルド，dune exec (/bin フォルダのファイルから .ml を取った名前)で実行
proof-ninja/whyml_sample
Folders and files
| Name | Name | Last commit date | ||
|---|---|---|---|---|
| Name | Name | Last commit date | ||
|---|---|---|---|---|
Why3 をライブラリとして使う OCamlのコードのサンプル
opam install . --deps-only でパッケージをインストール
why3 config detect を実行して Coq を認識させる
dune build でビルド， dune exec (/bin フォルダのファイルから .ml を取った名前) で実行