文件名称：experimental-coq-proofs:与Coq证明助手打交道
文件大小：7KB
文件格式：ZIP
更新时间：2024-06-09 15:32:39
Coq
实验性Coq证明 有关程序的定理，是使用编写的。 文件SfLib.v是一书中的开源帮助程序库。 与几乎所有Coq代码一样，该代码应使用或类的工具进行交互读取，该工具可以在代码的任何点向您显示当前的假设和证明目标。 它已通过Coq 8.4pl3（在Ubuntu 14.04上可用）进行了测试。 与往常一样，由于改进了标准库中的各种定理和求解器，因此更高版本有时会破坏更复杂的证明。 安装与入门 运行以下命令以安装编译器，并 sudo apt-get install coq coqc SfLib.v
【文件预览】：
experimental-coq-proofs-master
----.gitignore(12B)
----SfLib.v(8KB)
----LICENSE(1KB)
----SortedList.v(5KB)
----README.md(956B)