PHOAS dans Coq: incompatibilité de type

Question

Je transcris en Coq les définitions (informelles) du 2008 PHOAS paper, section 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. 

Sortie:

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

C'est plutôt désagréable. Comment puis-je faire ce type de code-vérifier?

Answer 1

Voici le code qui fonctionne:

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

Le problème est que vous essayez de construire une fonction (quelque chose du type forall) sans lambda (fun).

Answer 2

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