我正在研究Software Foundations书。在the chapter on polymorphism中,有一个关于“隐式参数”的部分。在本节中,有以下一行:
Arguments nil {X}.
当我尝试在
Poly.v
文件(本章的源代码,可在this tarball中使用)上运行Coq时,它停止在上述行中,出现错误:Error: No focused proof (No proof-editing in progress).
我已将
Poly.v
文件减少为仅包含以下内容,但仍给出相同的错误:Inductive list (X:Type) : Type :=
| nil : list X.
Arguments nil {X}.
关于此错误,我只能在Coq reference manual中找到的唯一内容是
我认为“证明编辑模式”是指使用战术证明定理的上下文。我不认为它处于这种模式,Coq也不会,因为它说“没有正在进行的证明编辑”。这是有道理的。
该错误声称
Arguments
是“证明编辑命令”,尽管在its documentation中并未说明,并且在the chapter on proof handling中未提及Arguments
。这使我认为Coq将
Arguments
错误地视为校对编辑命令,但我不知道为什么。我认为这一定是我的设置有问题,而不是
Poly.v
文件本身,因为它是《软件基础》一书的一部分。我正在使用CoqIDE,作为Coq 8.3pl4的一部分,随Ubuntu 12.04一起分发。 最佳答案
这是您使用的coq版本的问题。当前版本的Software Foundations仅与coq 8.4兼容。如果您想继续而不升级coq,则相关命令的旧版本为:
Implicit Arguments nil [[X]].
您可以在此处找到与您的coq版本兼容的poly.v的完整副本:
http://www.seas.upenn.edu/~cis500/cis500-s13/sf/Poly.html
玩得开心!
关于compiler-errors - 使用 “Error: No focused proof”命令时Coq “Arguments”,我们在Stack Overflow上找到一个类似的问题:https://stackoverflow.com/questions/20056972/