1 Nov
2016
1 Nov
'16
20:34
Ce problème est illustré par le test `let3` n'est-ce pas ?
Yes.
Je ne comprend pas pourquoi `OL.lexp_whnf idt (ectx_to_lctx ctx)` retourne la variable `TrueProp` et non l'expression que la variable contient.
Parce que lexp_check est appelé avec un lexp_context qui n'est pas encore complet: TrueProp y existe (il a type "Type") mais il est encore marqué ForwardRef plutôt que LetDef parce qu'on a pas fini de "lparse" toutes les définitions du groupe mutuellement récursif.
Stefan