Coq/Proof General中是否支持类似Agda的编程方式？
与Agda不同，Coq倾向于将证明与函数分开。Coq提供的策略非常适合编写证明，但我想知道是否有一种方法可以复制一些Agda-mode的功能。 具体来说，我想要： 一些类似于Agda的 ? 或 Haskell 的 _，在编写函数时可以省略部分内容，然后（希望）让Coq告诉我需要放置在那里...
我可以强制 Coq 打印括号吗？
我是Coq的新手，正在进行集合论证明的编写。 我发现公式中省略了括号，这使得我很难阅读公式。例如， 1 subgoal A, B : {set T} H : B \subset A ______________________________________(1/1) A :\: A :|...
参考文献“X”在当前环境中未找到。
我正在使用CoqIDE完成有关Coq的《软件基础》书中的练习。我可以成功编译Basics.v，结果为Basics.vo和Basics.glob在我的目录中。当我尝试运行Induction.v时，它可以正常工作。但是当我尝试编译它时，它会抱怨缺少大量引用，例如evenb和negb_involut...
CoqIDE加载ssreflect时的loadpath错误
我是Coq的新手，为了提高我的证明检查理解，我正在尝试使用Ssreflect库。 我已经在运行于终端的Mac OS v 10.10.3（Yosemite）上安装了Ssreflect v 1.5。 然而，当我尝试使用以下命令将库加载到CoqIDE 8.4p15中时： Require Imp...
如何高效地查找 Coq 中标识符的定义位置？
在大多数IDE或文本编辑器中，您可以右键单击术语，然后转到定义该术语的文件。但是CoqIDE似乎没有这个功能，所以我一直在使用coqdoc myfile.v --html，然后转到生成的HTML文档。但是，在该文件中，只有Coq标准库的术语可点击。由ssreflect定义的术语（例如）无法点击...