compiler-errors - 使用 "Error: No focused proof"命令时 Coq "Arguments"

Question

我正在处理 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 中找到的东西关于这个错误是

When one attempts to use a proof editing command out of the proof editing mode, Coq raises the error message : No focused proof.

我认为“证明编辑模式”是指使用策略证明定理的上下文。我不认为它处于那种模式，Coq 也没有，因为它说“没有正在进行的校对编辑”。所以这是有道理的。

错误声称 Arguments 是一个“校对编辑命令”，尽管它在 its documentation 中没有这样说, 并且 Arguments 在 the chapter on proof handling 中没有提到.

这使我认为 Coq 错误地将 Arguments 视为校对编辑命令，但我不知道为什么。

我认为这一定是我的设置有问题，而不是 Poly.v 文件本身有问题，因为它是《软件基础》一书的一部分。我正在使用 CoqIDE，作为 Coq 8.3pl4 的一部分，随 Ubuntu 12.04 一起分发。

Answer 1

这是您使用的 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

玩得开心!