| products/sources/formale Sprachen/Coq/test-suite/success/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: HoTT_coq_124.v Sprache: CoqOriginal von: Coq© |
|
||||||
|
(* 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" *) ¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
