coq:Coq是一个正式的证明管理系统。 它提供了一种正式的语言来编写数学定义可执行的算法和定理以及用于半交互式开发机器检查的证明的环境 源码

辅酶Q Coq是一个正式的证明管理系统。 它提供了一种正式的语言来编写数学定义,可执行算法和定理,以及用于半交互式开发机器检查的证明的环境。 安装 下载适用于Windows和macOS的的预构建软件包; 阅读有关如何使用Cop安装Coq的; 或参考文件以获取从源代码安装的过程。 文献资料 该文档的来源可以在目录找到。 请参阅以了解有关该文档的更多信息,尤其是如何构建它。 最新版本的文档可在Coq网站上网址为 。 另请参阅 (Coq Wiki)和 ,以获取其他用户提供的文档。 master分支的文档一直在部署。 看: 变化 参考手册的“一章说明了每个新版本的Coq的差异和不兼容之处。 如果您升级Coq,请仔细阅读,因为其中包含有关如何解决可能遇到的一些问题的重要建议。 问题与讨论 我们有多种渠道可以联系用户社区和开发团队: 我们的,用于休闲和繁忙的讨论。 我们的“ ,用于更结构