arguments - Coq --- 参数指令

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).

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

我正在使用 Coq 版本 8.3pl4 和 CoqIDE 编辑器。

Answer 1

我只是在我的（有点旧的）Coq 8.4 上尝试过，我对隐式声明没有任何问题。但是，如果我写Argument而不是Arguments（注意缺少“s”），我会得到

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

你拼写正确吗？

编辑：对不起，我错过了你的版本。似乎该Arguments命令已在 8.4 后添加（它没有出现在此处但出现在此处。我建议您尽可能更新您的 Coq 版本，或限制使用 8.3Implicit相关命令（疯狂猜测Implicit Arguments foo.：）