我正在研究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/

10-12 18:48