PHOAS in Coq：type mismatch

我在Coq中抄錄了2008 PHOAS paper第2.1節中的（非正式）定義。PHOAS in Coq：type mismatch

Inductive tm' {V : Set} : Set := 
| Var : V -> tm' 
| App : tm' -> tm' -> tm' 
| Abs : (V -> tm') -> tm'. 

Definition tm := forall X, @tm' X. 

Fail Example id : tm := Abs Var.

輸出：

The term "Abs Var" has type "tm'" while it is expected to have type "tm".

這是相當討厭。我怎樣才能使這種代碼類型檢查？

來源

2017-06-26 Carl Patenaude Poulin

這裏是代碼的工作：

Example id : tm := fun _ => Abs Var.

的問題是，你試圖構建一個功能（類型forall的東西）沒有一個lambda（fun）。

來源

2017-07-28 04:37:03

Example id : tm := fun (X : Set) => Abs Var.

來源

2017-06-26 17:41:00

請使用您問題上的編輯鏈接添加其他信息。後回答按鈕應該只用於問題的完整答案。 - [來自評論]（/ review/low-quality-posts/16533671） –

從Jason Gross的回答可以看出，這確實是一個完整的答案。 –

PHOAS in Coq：type mismatch

回答

相關問題