Coq --- Arguments directive

Question

我正在阅读《软件基础》一书，发现了一个声明参数的命令隐含：

Arguments nil {X}.

其中，例如：

Inductive list (X:Type) : Type :=
| nil : list X
| cons : X -> list X -> list X.

然而，每当我尝试执行这样的命令时，我都会收到以下消息：

Error: No focused proof (No proof-editing in progress).

即使我试图编译这本书附带的脚本，也会出现同样的消息。可能是什么问题？

我使用的是Coq8.3pl4版本和CoqIDE编辑器。

Answer 1

我刚刚在我的（有点旧的）Coq8.4上尝试了它，我对隐式声明没有任何问题。但是，如果我写Argument而不是Arguments（注意缺少"s"），我会得到

Error: Unknown command of the non proof-editing mode.

你拼写对了吗？

编辑：对不起，我错过了你的版本。Arguments命令似乎是在8.4之后添加的（它没有出现在这里，但出现在这里。如果可能的话，我建议您更新您的Coq版本，或者限制使用8.3 Implicit相关命令（猜测：Implicit Arguments foo.）