|
Require Coq.Classes.RelationClasses.
Class PreOrder (A : Type) (r : A -> A -> Type) : Type :=
{ refl : forall x, r x x }.
(* FAILURE 1 *)
Section foo.
Polymorphic Universes A.
Polymorphic Context {A : Type@{A}} {rA : A -> A -> Prop} {PO : PreOrder A rA}.
Fail Definition foo := PO.
End foo.
Module ILogic.
Set Universe Polymorphism.
(* Logical connectives *)
Class ILogic@{L} (A : Type@{L}) : Type := mkILogic
{
lentails: A -> A -> Prop;
lentailsPre:> RelationClasses.PreOrder lentails
}.
End ILogic.
Set Printing Universes.
(* There is still a problem if the class is universe polymorphic *)
Section Embed_ILogic_Pre.
Polymorphic Universes A T.
Fail Context {A : Type@{A}} {ILA: ILogic.ILogic@{A} A}.
End Embed_ILogic_Pre.
¤ Dauer der Verarbeitung: 0.21 Sekunden
(vorverarbeitet)
¤
|
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.
|
