|
(** Omega is now aware of the bodies of context variables
(of type Z or nat). *)
Require Import ZArith Omega.
Open Scope Z.
Goal let x := 3 in x = 3.
intros.
omega.
Qed.
Open Scope nat.
Goal let x := 2 in x = 2.
intros.
omega.
Qed.
(** NB: this could be disabled for compatibility reasons *)
Unset Omega UseLocalDefs.
Goal let x := 4 in x = 4.
intros.
Fail omega.
Abort.
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
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.
|
