为什么我的定义因为严格的正性条件而被禁止？
我有以下两个定义，导致了两个不同的错误信息。 第一个定义被拒绝是因为严格的正性，第二个定义是因为宇宙不一致性。(* non-strictly positive *) Inductive SwitchNSP (A : Type) : Type := | switchNSP : SwitchNSP...
像Coq这样的非图灵完备语言有哪些实际限制？
由于存在非图灵完备语言，而且我没有在大学学习计算机科学，能否有人解释一下图灵不完备语言（如Coq）不能做什么？ 或者说完备性/不完备性在实际中并不真正重要吗？ 编辑 - 我想要一个回答，类似于“由于X的原因，在非图灵完备语言中无法构建哈希表”，或者类似的回答！
Z3和Coq之间的区别
我想知道有没有人能告诉我Z3和coq之间的区别？ 在我看来，coq是一种证明助手，因为它要求用户填写证明步骤，而Z3则没有这个要求。 但似乎coq也具有类似于Z3的自动策略吗？ 或者说coq中的证明搜索能力不如Z3强大？
当使用依赖类型语言编程时，我们如何克服编译时间和运行时间之间的差距？
据我所知，在依赖类型系统中，“类型”和“值”被混合在一起，我们可以将它们都视为“术语”。 但是有些事情我不太理解：在没有依赖类型的强类型编程语言（如Haskell）中，类型在编译时被确定（推断或检查），而值在运行时被确定（计算或输入）。 我认为这两个阶段之间必须存在差距。如果一个值是交互式...
类型参数和索引的区别是什么？
我对依赖类型还不熟悉，对于两者之间的区别感到困惑。似乎人们通常说一个类型是由另一个类型参数化和由某个值索引。但是，在依赖类型的语言中，类型和术语之间是没有区别的，对吗？参数和索引之间的区别是否是基本的？您能否为我展示一些编程和定理证明中意义差异的例子？
Coq和Agda之间的区别
这些程序各自设计用于什么，并且它们各自提供了什么？此外，两个系统是否一致，并且它们是否基于某种基础数学理论？ 我关心的两件事： 易于安装 易于学习 我已经进行了搜索，所读到的似乎非常极端，我想从最客观（人类）的角度了解它们之间的区别。
在Coq中，`true = false`是什么意思？
[我不确定这是否适合于stackoverflow，但是由于其他Coq问题在这里有很多，所以也许有人可以帮助。] 我正在按照http://www.cis.upenn.edu/~bcpierce/sf/Basics.html#lab28中介绍的步骤进行工作（就在Case之后）。请注意，我是一个完...
为什么较新的依赖类型语言没有采用SSReflect的方法？
在Coq的SSReflect扩展中，我发现了两种约定，它们似乎特别有用，但我没有看到它们被广泛采用于新的依赖类型语言（如Lean、Agda、Idris）。首先，尽可能使用返回布尔值的函数来表示谓词，而不是归纳定义数据类型。这默认带来可决定性，为计算证明提供了更多机会，并通过避免证明引擎携带大型...
我能把Coq的证明提取成Haskell函数吗？
自从我学了一点Coq，我就想学习编写所谓的除法算法的Coq证明： forall n m : nat, exists q : nat, exists r : nat, n = q * m + r 最近我用Software Foundations学到的知识完成了这个任务。 Coq是一个开发构造性...