Директива Coq Arguments

Я читаю книгу Основы программного обеспечения и наткнулся на команду, которая объявляет параметры как неявные :

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.


arguments implicit-typing coq
person bellpeace    schedule 25.04.2014    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Я просто попробовал это на моем (несколько старом) Coq 8.4, и у меня нет проблем с неявным объявлением. Однако если я напишу Argument вместо Arguments (обратите внимание на отсутствие "s"), я получу

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

Вы правильно написали?

РЕДАКТИРОВАТЬ: извините, я пропустил вашу версию. Похоже, что команда Arguments была добавлена ​​в сообщение 8.4 (она не отображается здесь, но отображается здесь. Советую обновить Версия Coq, если возможно, или ограничьте использование связанных команд 8.3 Implicit (безумное предположение: Implicit Arguments foo.)

person Vinz    schedule 28.04.2014
comment
Я использую Arguments. Я думаю, что пишу правильно, так как использую сценарии, которые поставляются с книгой. - person bellpeace; 28.04.2014
comment
Я отредактировал свой ответ, похоже, команда, которую вы хотите использовать, не существует в версии Coq, которую вы используете. - person Vinz; 30.04.2014