錯誤：非法應用（非功能性構造）

我正在嘗試使用HoTT書籍中的類型構造函數/消除器來闡述各種deMorgans法則的一些證明。我已經跳過了相關的東西挑選https://mdnahas.github.io/doc/Reading_HoTT_in_Coq.pdf並將其全部轉儲到.v文本文件中。我需要消除/介紹產品，聯產品和建立否定的方法規則。到目前爲止，我有，錯誤：非法應用（非功能性構造）

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.

上的錯誤「的定義FST（P：A * B）：=」是

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

我試圖通過錯誤列表上勒柯克現場尋找，但沒」找不到任何東西。

來源

2017-10-07 bkbowser

如果下面貼的回答幫你解決問題，那麼它會是不錯的，如果你接受了答案。 –

有兩個問題與您的代碼：

prod的兩家Type參數聲明隱含

因此，符號"x * y"對應prod {_} {_} x y將總是導致虐待鍵入術語：prod {_} {_}是Type，因此將它應用於某些內容是沒有意義的。

的解決方法是將這些兩個隱含參數轉化爲顯性的：

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

記號(x , y)尚未聲明

一旦你固定的prod的定義，定義仍然不要typecheck，因爲Coq不知道你的意思是(x, y)的模式。您可以將您Section projections之前聲明它作爲一個新的符號，像這樣：

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

來源

2017-10-07 19:36:26 gallais

錯誤：非法應用（非功能性構造）

回答

相關問題