..

Why3 安装

Why3 官网 ： https://www.why3.org/

Why3 文档： https://www.why3.org/doc/

why3 安装：

opam install why3

安装IDE：

opam install why3-ide

安装完成后手动配置prover：

why3 config add-prover  <name> <path> [shortcut]

why3 config list-supported-provers可列出why3支持的prover

也可自动配置prover：

why3 config detect

如果需要在why3中调用Coq进行交互式证明需要安装why3-coq：

opam install coq
opam install coqide
opam install why3-coq

此时右键菜单显示可使用的prover。

点击Coq 8.19.1即可使用Coq进行交互式证明。