Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/Roqc/vernac/ (Beweissystem des Inria Version 9.1.0^©) Datei vom 15.8.2025 mit Größe 3 kB

Quelle univscompute.v Sprache: 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.

quality98%

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