Coq 中的 PHOAS：类型不匹配答案

【问题标题】：PHOAS in Coq: type mismatchCoq 中的 PHOAS：类型不匹配
【发布时间】：2017-06-26 17:30:04
【问题描述】：

我正在 Coq 中转录 2008 PHOAS paper 第 2.1 节中的（非正式）定义。

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".

那是相当讨厌的。如何进行此代码类型检查？

【问题讨论】：

标签： coq

【解决方案1】：

这是有效的代码：

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

问题是您试图构造一个没有 lambda (fun) 的函数（forall 类型的东西）。

【讨论】：

【解决方案2】：

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

【讨论】：

请使用您问题上的编辑链接添加更多信息。 Post Answer 按钮应仅用于问题的完整答案。 - From Review
从 Jason Gross 的回答中可以看出，这确实是一个完整的答案。