Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: nc106a.cob Sprache: Coq

Original von: Coq^©

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.46 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.