私はソフトウェアの基礎の本を読んでいて、パラメーターを暗黙的として宣言するコマンドに出くわしました:
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 エディターを使用しています。