我希望有一个归纳类型来描述排列及其对某些容器的作用。很明显，根据这个类型的描述，算法的定义复杂度（以长度衡量）（计算组合或逆，分解为不相交的循环等）将会有所不同。 考虑在Coq中以下定义。我认为它是Lehmer编码的形式化：Inductive Permutation : nat -> S...

假设我有一个任意的 Coq 术语（使用 s-表达式/sexp 格式的 AST）： n = n + n 我想通过遍历 AST 树（由于 sexp，它只是一个嵌套列表的列表）来自动将其转换为： = n + n n 在 Python 中是否有标准库可以做到这一点？ 如果我要写下算法/伪代码...

假设我已经在Coq中证明了某个定理，并且后来我想将其作为另一个定理的假设引入。有没有一种简洁的方法可以做到这一点？ 我通常需要这样做是因为我想进行类似于按情况证明的操作。我发现一种方法是用assert断言定理的陈述，然后立即证明它，但这似乎有些繁琐。例如，我倾向于写出这样的内容:Requir...

如标题所示，Coq能用作模型检查器吗？我能将模型检查与Coq证明混合使用吗？这种做法常见吗？Google提到了“µ-演算”，有人对此或类似的东西有经验吗？建议以这种方式使用Coq，还是应该寻找其他工具？

.v 是用于验证或者检验吗？是在走吧（vamanos）吗？ 为什么不使用 .coq 扩展名呢？

有人知道以下内容的示例吗？ 在证明助手（例如Coq）中，关于正则表达式（可能扩展为反向引用）的证明开发。 使用依赖类型语言（例如Agda）编写的关于正则表达式的程序。

我无法在CoqIde中加载与当前文件夹相同的模块。 我正在尝试从Software Foundations中加载源代码，我在包含SF源代码的文件夹中使用coqide或coqide ./运行CoqIde，然后打开并运行文件，但是我遇到了这个错误：Error: Cannot find librar...

我们如何获取诸如"+"或"++"这样的符号在List中的定义/类型？ 我尝试过：Search ++、Search "++"、Search (++)、SearchAbout ...以及Check ++、Check "++"、Check(++)。但是它们都没有起作用... SearchAbout ...

我还对 Coq 中的 "Set" 类型有些困惑。我应该什么时候使用 "Set"，什么时候使用 "Type"？ 在 Hott 中，"Set" 被定义为一个类型，在该类型中，身份证明是唯一的。 但我认为在 Coq 中它有一个不同的解释。

我正在使用JavaScript实现算法W（Hindley-Milner类型系统）： 实现上述规则的函数是typecheck，其签名如下： typecheck :: (Context, Expr) -> Monotype 它的定义如下： function typecheck(...