diff options
Diffstat (limited to 'test-suite/success/tryif.v')
-rw-r--r-- | test-suite/success/tryif.v | 50 |
1 files changed, 50 insertions, 0 deletions
diff --git a/test-suite/success/tryif.v b/test-suite/success/tryif.v new file mode 100644 index 00000000..4394bddb --- /dev/null +++ b/test-suite/success/tryif.v @@ -0,0 +1,50 @@ +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. |