Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: dump.scala Sprache: Coq

Original von: Coq^©

Require Import TestSuite.admit.

(** [not tac] is equivalent to [fail tac "succeeds"] if [tac] succeeds, and is equivalent to [idtac] if [tac] fails *)
Tactic Notation "not" tactic3(tac) :=
  (tryif tac then fail 0 tac "succeeds" else idtac); (* error if the tactic solved all goals *) [].

(** Test if a tactic succeeds, but always roll-back the results *)
Tactic Notation "test" tactic3(tac) := tryif not tac then fail 0 tac "fails" else idtac.

Goal Set.
Proof.
  not fail.
  not not idtac.
  not fail 0.
  (** Would be nice if we could get [not fail 1] to pass, maybe *)
  not not admit.
  not not test admit.
  not progress test admit.
  (* test grouping *)
  not (not idtac; fail).
  assert True.
  all:not fail.
  2:not fail.
  all:admit.
Defined.

Goal Set.
Proof.
  test idtac.
  test try fail.
  test admit.
  test match goal with |- Set => idtac end.
  test (idtac; match goal with |- Set => idtac end).
  (* test grouping *)
  first [ (test idtac; fail); fail 1 | idtac ].
  try test fail.
  try test test fail.
  test test idtac.
  test test admit.
  Fail test fail.
  test (idtac; []).
  test (assert True; [|]).
  (* would be nice, perhaps, if we could catch [fail 1] and not just [fail 0] this *)
  try ((test fail); fail 1).
  assert True.
  all:test idtac.
  all:test admit.
  2:test admit.
  all:admit.
Defined.

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