Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma

Benutzer


products/Sources/formale Sprachen/Roqc/test-suite/success/ (NIST Cobol Test-Suite ^©) 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 *) : Type, T -> T) (fun T:Type (* u1 *) => K T))"
   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"
*)

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.8 Sekunden (vorverarbeitet am 2026-09-28) ¤

Wurzel

Suchen

PVS Prover

Isabelle Prover

NIST Cobol Testsuite

Cephes Mathematical Library

Vienna Development Method

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.