Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: univscompute.v Sprache: Coq

Original von: Coq^©

Set Universe Polymorphism.

Polymorphic Definition id {A : Type} (a : A) := a.

Eval vm_compute in id 1.

Polymorphic Inductive ind (A : Type) := cons : A -> ind A.

Eval vm_compute in ind unit.

Check ind unit.

Eval vm_compute in ind unit.

Definition bar := Eval vm_compute in ind unit.
Definition bar' := Eval vm_compute in id (cons _ tt).

Definition bar'' := Eval native_compute in id 1.
Definition bar''' := Eval native_compute in id (cons _ tt).

Definition barty := Eval native_compute in id (cons _ Set).

Definition one := @id.

Monomorphic Definition sec := one.

Eval native_compute in sec.
Definition sec' := Eval native_compute in sec.
Eval vm_compute in sec.
Definition sec'' := Eval vm_compute in sec.

¤ 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.