Quelle DeclareSort.v Sprache: Coq

Sort s.
Sort s'.

Fail Check fun (A:Type@{s;Set}) => A : Type@{s';_}.

Fail Check fun (A:Type@{s;Set}) => A : Type.

Fail Check fun (A:Set) => A : Type@{s;_}.

Check fun (A:Type@{s;Set}) => A : Type@{s;_}.

Section S.
  Sort S1.
  Local Set Universe Polymorphism.
  Sort S2.

  Axiom foo : Type@{S1;Set} -> Type@{S2;Set}.
  Check foo.

End S.

About foo.
Set Printing Universes.
About foo.

Check foo : _ -> SProp.
Check foo : _ -> Set.

Fail Check foo : SProp -> _.
Fail Check foo : Set -> _.
Check foo : Type@{S1;Set} -> Set.

Module Type T.
  Module M.
    Fail Sort foz.
  End M.
End T.

quality100%

¤ Dauer der Verarbeitung: 0.3 Sekunden ¤

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.