Quelle bug_5726.v Sprache: Coq

Set Universe Polymorphism.
Set Printing Universes.

Module GlobalReference.

  Definition type' := Type.
  Notation type := type'.
  Check type@{Set}.

End GlobalReference.

Module TypeLiteral.

  Notation type := Type.
  Check type@{Set}.
  Check type@{Prop}.

End TypeLiteral.

Module ExplicitSort.
  Monomorphic Universe u.
  Notation foo := Type@{u}.
  Fail Check foo@{Set}.
  Fail Check foo@{u}.

  Notation bar := Type.
  Check bar@{u}.
End ExplicitSort.

Module PropNotationUnsupported.
  Notation foo := Prop.
  Fail Check foo@{Set}.
  Fail Check foo@{Type}.
End PropNotationUnsupported.

quality100%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.