Why3 をライブラリとして使う OCamlのコードのサンプル
-
opam install . --deps-onlyでパッケージをインストール -
why3 config detectを実行して Coq を認識させる -
dune buildでビルド，dune exec (/bin フォルダのファイルから .ml を取った名前)で実行 -
why3 pp --output=sexp (mlw ファイル)で具体的な WhyML のコードがどのように Ptree の項にされているかが見られるので，参考に．