文件名称：coq-wrengr-util:Coq 的策略、效用引理和关系组合器
文件大小：53KB
文件格式：ZIP
更新时间：2024-07-02 10:54:12
Coq
描述 该库提供了实用策略和引理的集合。 这里没有什么特别特别的地方，但它们非常有用并且经常在我的代码中使用。 ./src/Tactics 该Tactics.Core模块包含了一些非常简单的战术，我使用非常频繁，如引进的变量只是叫自毁/反转/感应就可以了，或者insist的策略是一样exact ，只是它会用congruence证明你坚持的假设可以改写为当前的目标。 Tactics.Destroy模块定义了destruct_if策略，它将在目标中查找 if-then-else 项，破坏他们的被审查者，然后进行一些清理，这通常有助于实现子目标。 Tactics.ExFalso模块定义了ex_falso策略，该策略寻找矛盾并使用它们来实现当前目标。 Tactics.Fequal模块定义了fequal策略，它是内置f_equal策略的改进版本。 Tactics.Introv模块定义了在So
【文件预览】：
coq-wrengr-util-master
----.gitignore(217B)
----Makefile(8KB)
----src()
--------Relations()
--------CoqExtras()
--------Tactics()
----.travis.yml(2KB)
----TODO(184B)
----LICENSE(2KB)
----README.md(5KB)
----LICENSE-LGPLv3(7KB)
----LICENSE-BSD3(2KB)