products/sources/formale Sprachen/Cobol/Test-Suite/SQL M/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: cumpoly.v   Sprache: Unknown

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.1 Sekunden  (vorverarbeitet)  ]