COQ --- 인수 내가 <a href="http://www.cis.upenn.edu/~bcpierce/sf/" rel="nofollow">Software foundations</a> 책을 읽고 그리고 난이 같은 암시 적 변수 선언 명령 건너 온

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에서 시도했지만 암묵적인 선언에는 아무런 문제가 없습니다. 그러나 내가 대신 Arguments의 Argument는 ("S"의 부족을 통지) 작성하는 경우, 나는

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

당신이 그것을 정확하게 철자나요거야?

편집 : 죄송합니다. 버전을 놓친 것 같습니다. Arguments 명령이 here을 here을 표시하지만 표시되지 않습니다 (8.4 POST 추가 된 것 같습니다 당신이 가능한 경우 COQ 버전을 업데이트하거나 (8.3 Implicit 관련 명령을 사용하여 추측 제한 조언 :.