Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: unidecls.v Sprache: Coq

Original von: Coq^©

(* -*- coq-prog-args: ("-top" "unidecls"); -*- *)
Set Printing Universes.

Module decls.
  Universes a b.
End decls.

Universe a.

Constraint a < decls.a.

Print Universes.

(** These are different universes *)
Check Type@{a}.
Check Type@{decls.a}.

Check Type@{decls.b}.

Fail Check Type@{decls.c}.

Fail Check Type@{i}.
Universe foo.
Module Foo.
  (** Already declared globaly: but universe names are scoped at the module level  *)
  Universe foo.
  Universe bar.

  Check Type@{Foo.foo}.
  Definition bar := 0.
End Foo.

(** Already declared in the module *)
Universe bar.

(** Accessible outside the module: universe declarations are global *)
Check Type@{bar}.
Check Type@{Foo.bar}.

Check Type@{Foo.foo}.
(** The same *)
Check Type@{foo}.
Check Type@{unidecls.foo}.

Universe secfoo.
Section Foo'.
  Fail Universe secfoo.
  Universe secfoo2.
  Fail Check Type@{Foo'.secfoo2}.
  Check Type@{secfoo2}.
  Constraint secfoo2 < a.
End Foo'.

Check Type@{secfoo2}.
Fail Check eq_refl : Type@{secfoo2} = Type@{a}.

(** Below, u and v are global, fixed universes *)
Module Type Arg.
  Universe u.
  Parameter T: Type@{u}.
End Arg.

Module Fn(A : Arg).
  Universes v.

  Check Type@{A.u}.
  Constraint A.u < v.

  Definition foo : Type@{v} := nat.
  Definition bar : Type@{A.u} := nat.

  Fail Definition foo(A : Type@{v}) : Type@{A.u} := A.
End Fn.

Module ArgImpl : Arg.
  Definition T := nat.
End ArgImpl.

Module ArgImpl2 : Arg.
  Definition T := bool.
End ArgImpl2.

(** Two applications of the functor result in the exact same universes *)
Module FnApp := Fn(ArgImpl).

Check Type@{FnApp.v}.
Check FnApp.foo.
Check FnApp.bar.

Check (eq_refl : Type@{ArgImpl.u} = Type@{ArgImpl2.u}).

Module FnApp2 := Fn(ArgImpl).
Check Type@{FnApp2.v}.
Check FnApp2.foo.
Check FnApp2.bar.

Import ArgImpl2.
(** Now u refers to ArgImpl.u and ArgImpl2.u *)
Check FnApp2.bar.

(** It can be shadowed *)
Universe u.

(** This refers to the qualified name *)
Check FnApp2.bar.

Constraint u = ArgImpl.u.
Print Universes.

Set Universe Polymorphism.

Section PS.
  Universe poly.

  Definition id (A : Type@{poly}) (a : A) : A := a.
End PS.
(** The universe is polymorphic and discharged, does not persist *)
Fail Check Type@{poly}.

Print Universes.
Check id nat.
Check id@{Set}.

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