Quelle section_poly.v Sprache: Coq

Section Foo.

  Variable X : Type.

  Polymorphic Section Bar.

  Variable A : Type.

  Definition id (a:A) := a.

End Bar.
Check id@{_}.
End Foo.
Check id@{_}.

Polymorphic Section Foo.
Variable A : Type.
Section Bar.
  Variable B : Type.

  Inductive prod := Prod : A -> B -> prod.
End Bar.
Check prod@{_}.
End Foo.
Check prod@{_ _}.

Section Foo.

  Universe K.
  Inductive bla := Bla : Type@{K} -> bla.

  Polymorphic Definition bli@{j} := Type@{j} -> bla.

  Definition bloo := bli@{_}.

  Polymorphic Universe i.

  Fail Definition x := Type.
  Fail Inductive x : Type := .
  Polymorphic Definition x := Type.
  Polymorphic Inductive y : x := .

  Variable A : Type. (* adds a mono univ for the Type, which is unrelated to the others *)

  Fail Variable B : (y : Type@{i}).
  (* not allowed: mono constraint (about a fresh univ for y) regarding
  poly univ i *)

  Polymorphic Variable B : Type. (* new polymorphic stuff always OK *)

  Variable C : Type@{i}. (* no new univs so no problems *)

  Polymorphic Definition thing := bloo -> y -> A -> B.

End Foo.
Check bli@{_}.
Check bloo@{}.

Check thing@{_ _ _}.

Section Foo.

  Polymorphic Universes i k.
  Universe j.
  Fail Constraint i < j.
  Fail Constraint i < k.

  (* referring to mono univs in poly constraints is OK. *)
  Polymorphic Constraint i < j. Polymorphic Constraint j < k.

  Polymorphic Definition foo := Type@{j}.
End Foo.

quality100%

¤ Dauer der Verarbeitung: 0.4 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.