Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Sprache: Coq

Original 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.15 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

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 ist noch experimentell.