Quelle bug_12948.v Sprache: Coq

(* -*- coq-prog-args: ("-noinit"); -*- *)

Example simple_cbn := Eval cbn in (fun x:Set => x).

Definition id {A} (x:A) := x.
Definition set := Eval lazy in id Set.

Compute id Set.

Require Import Prelude.

Goal Prop.
let c := eval unfold set in set in
constr_eq c Set.
Abort.

quality99%

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