文件名称：coq-ltac2-experiments:我用Ltac2编写的所有代码
文件大小：11KB
文件格式：ZIP
更新时间：2024-06-15 23:22:27
coq ltac2 Coq
Ltac2实验 您可能还想看看我写的《 。 实现从Gallina字符串到Gallina标识符的转换，并将此功能导出到Ltac1。 匹配目标和操纵假设的示例。 假设中存在一种破坏性策略，可以保留现有名称。 说明了从活页夹获取标识符，将ident变量传递给原始策略以及生成新名称的方法。 提供足够的Ltac1功能以使Software Foundations正常运行的库。 包含一条注释，解释如何处理其他一些无法通过代码解决的不兼容问题（或者至少我不知道如何解决）。 演示如何使用Ltac2策略包装Ltac1。 这比使用Ltac2证明脚本中的ltac1:(...)更为复杂，在ltac1:(...)脚本中ltac1:(...)通常可以工作，因为包装器必须是一个封闭值。 尝试对Ltac2做任何事情的各种实验。
【文件预览】：
coq-ltac2-experiments-master
----.gitignore(42B)
----README.md(1KB)
----_CoqProject(24B)
----src()
--------Ltac2Lib.v(4KB)
--------congruence.v(190B)
--------backtrack.v(507B)
--------deex.v(2KB)
--------backtrace.v(322B)
--------playground.v(2KB)
--------matching.v(2KB)
--------char.v(4KB)
--------string.v(4KB)
----.travis.yml(861B)
----Makefile(513B)