| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/test-suite/modules/ (Beweissystem des Inria Version 9.1.0©) Datei vom 15.8.2025 mit Größe 614 B |
|
Quelle cumpoly.v Sprache: Coq |
|||||||||
|
Set Universe Polymorphism.
(** Check that variance subtyping is respected. The signature T is asking for invariance, while M provide an irrelevant implementation, which is deemed legit. There is currently no way to go the other way around, so it's not possible to generate a counter-example that should fail with the wrong subtyping. *) Module Type T. Parameter t@{i|Set <= i} : Type@{i}. Cumulative Inductive I@{i|Set <= i} : Type@{i} := C : t@{i} -> I. End T. Module M : T. Definition t@{i|Set <= i} : Type@{i} := nat. Cumulative Inductive I@{i|Set <= i} : Type@{i} := C : t@{i} -> I. End M. ¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28