Coq --- 参数指令

【问题标题】：Coq --- Arguments directiveCoq --- 参数指令
【发布时间】：2014-04-25 21:56:45
【问题描述】：

我正在阅读Software foundations 的书，我遇到了一个声明参数的命令作为隐含的：

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 编辑器。

【问题讨论】：

【解决方案1】：

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

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

你写对了吗？

编辑：对不起，我错过了阅读您的版本。似乎Arguments 命令已在 8.4 之后添加（它没有出现 here 但出现 here。我建议您尽可能更新您的 Coq 版本，或者限制使用 8.3 的 Implicit 相关命令（猜测:Implicit Arguments foo.)

【讨论】：