(* This example used to emphasize the absence of LEGO-style universe polymorphism; Matthieu's improvements of typing on 2011/3/11 now makes (apparently) that Amokrane's automatic eta-expansion in the coercion mechanism works; this makes its illustration as a "weakness" of universe polymorphism obsolete (example submitted by Randy Pollack).
Note that this example is not an evidence that the current non-kernel eta-expansion behavior is the most expected one.
*)
Parameter K : forall T : Type, T -> T. Check (K (forall T : Type, T -> T) K).
(* note that the inferred term is
"(K (forall T (* u1 *)
which is not eta-equivalent to "(K (forall T : Type, T -> T) K"
because the eta-expansion of the latter "(K (forall T : Type, T -> T) (fun T:Type (* u2 *) => K T)"
assuming K of type"forall T (* u2 *) : Type, T -> T"
*)
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
