오류 : 불법 응용 프로그램 (비 기능적 구성)

Question

HoTT 북에서 형식 생성자/제거기를 사용하여 다양한 deMorgans 법칙에 대한 몇 가지 증명을하려고합니다. 나는 관련 자료에 대해 https://mdnahas.github.io/doc/Reading_HoTT_in_Coq.pdf을 선택하여 .v 텍스트 파일로 모두 넘겼습니다. 제품, 공동 제품 및 부정을 설정하는 방법에 대한 제거/소개 규칙이 필요합니다. ' "= (: A *의 B p)의 정의 FST"

Error: Illegal application (Non-functional construction): 
The expression "prod" of type "Type" 
cannot be applied to the term 
"A" : "Type" 

나는 COQ 사이트에서 오류 목록을 검색하려했지만 didn를하다 지금까지 나는

Definition idmap {A:Type} (x:A) : A := x. 

Inductive prod {A B:Type} : Type := pair : A -> B -> @prod A B. 

Notation "x * y" := (prod x y) : type_scope. 

Section projections. 
    Context {A : Type} {B : Type}. 
    Definition fst (p: A * B) := 
    match p with 
     | (x , y) => x 
    end. 

    Definition snd (p:A * B) := 
    match p with 
     | (x , y) => y 
    end. 
End projections. 

에 오류가 있습니다 아무것도 찾지 마라.

Answer 1

은 당신의 코드에 두 가지 문제가 있습니다

• prod의 두 Type 인수가

결과적으로 암시 적 선언, 항상를 변이로 이어질 것입니다 "x * y"이 prod {_} {_} x y에 해당하는 표기 입력 된 단어 : prod {_} {_}은 Type이므로 뭔가를 적용하는 것이 적절하지 않습니다.

수정 프로그램은 명시적인 것들로이 두 암시 인수를 설정하는 것입니다 :

Inductive prod (A B:Type) : Type := pair : A -> B -> @prod A B. 

• 당신이 prod의 정의를 수정 한 후 (x , y)는

선언되지 않은 표기는 Coq는 당신이 패턴 (x, y)의 의미를 알지 못하기 때문에 여전히 typecheck를하지 않습니다. 당신은 너무처럼 Section projections 전에 새 표기법으로 선언 할 수 있습니다 : 아래 게시 된 대답은 당신이 당신의 문제를 해결하는 데 도움이

Notation "x , y" := (pair _ _ x y) (at level 10).