文件名称：exceptional-tt:在 Coq 中实现异常的 Coq 插件
文件大小：32KB
文件格式：ZIP
更新时间：2024-06-18 14:12:50
OCaml
Coq 中合理的异常类型理论 这个插件允许自动翻译 Coq 术语，以便它们现在可以以受控方式使用异常。 这对于编程很有用，例如允许本地失败并在假设一些属性后证明翻译的术语不会失败，不会危及减少或污染类型签名，就像一元翻译会做的那样。 可以在找到描述翻译的草稿。 汇编 这需要 Coq 8.8。 如果COQBIN变量设置正确，则调用make就足够了。 或者，可以通过 OPAM 安装此插件。 假设 Coq 存储库可用（请参阅），执行以下操作就足够了。 opam pin add coq-exceptional-tt https://github.com/CoqHott/exceptional-tt.git opam install coq-exceptional-tt 插件的使用 该插件添加了我们下面将介绍的新的本地命令。 效果翻译 Effect Translate GLOBAL [us
【文件预览】：
exceptional-tt-master
----_CoqProject(185B)
----theories()
--------Effects.v(5KB)
----COPYING(484B)
----opam(607B)
----agda-rr()
--------ett-rr.agda(4KB)
--------cast-cic.agda(7KB)
----src()
--------eTranslate.ml(50KB)
--------eUtil.ml(8KB)
--------exception.mlpack(37B)
--------g_exception.ml4(1KB)
--------ePlugin.ml(16KB)
--------eUtil.mli(333B)
--------ePlugin.mli(260B)
--------eTranslate.mli(2KB)
----Dockerfile(282B)
----README.md(3KB)
----Makefile(252B)
----tests()
--------list_theorem.v(9KB)
--------Makefile(306B)
----.gitignore(168B)
----.gitlab-ci.yml(262B)