| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/test-suite/success/ (Beweissystem des Inria Version 9.1.0©) Datei vom 15.8.2025 mit Größe 914 B |
|
Quelle universes_coercion.v Sprache: 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.13 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-04-04