文件名称：proofs:Coq中的一系列正式证明
文件大小：50KB
文件格式：ZIP
更新时间：2024-05-26 04:35:02
coq proof-assistant type-theory formal-verification Coq
证明 中形式证明的选择。 指示 确保您具有下面列出的依赖项。 然后，您可以运行make来验证证明。 您还可以使用make lint调用短绒。 可以使用make clean构建工件。 依存关系 构建系统取决于以下内容： > = 3.79.1 > = 8.7.2 您还需要一套常用的Unix工具，例如echo ， find等。
【文件预览】：
proofs-main
----.gitignore(164B)
----toast.yml(2KB)
----Makefile(1KB)
----_CoqProject(46B)
----LICENSE.md(1KB)
----.travis.yml(595B)
----.github()
--------workflows()
----proofs()
--------Reflection()
--------Kleene()
--------Intro()
--------Tactics.v(4KB)
--------Metatheory()
--------STLC()
--------SystemF()
--------CategoryTheory()
----scripts()
--------lint-general.rb(2KB)
--------lint-imports.rb(2KB)
----README.md(708B)