diff --git a/tests/8pus/bad/no_arg_tactic.8pus b/tests/8pus/bad/no_arg_tactic.8pus new file mode 100644 index 0000000..4ac19d8 --- /dev/null +++ b/tests/8pus/bad/no_arg_tactic.8pus @@ -0,0 +1,6 @@ +Goal A -> B -> C -> A. +intros. + apply. + exact. +assumption. +Qed. \ No newline at end of file diff --git a/tests/8pus/bad/not_yet_qed.8pus b/tests/8pus/bad/not_yet_qed.8pus new file mode 100644 index 0000000..c0b7a3f --- /dev/null +++ b/tests/8pus/bad/not_yet_qed.8pus @@ -0,0 +1,4 @@ +Goal A -> B -> A. +intros. +Qed. +Check. \ No newline at end of file diff --git a/tests/8pus/bad/undo_empty.8pus b/tests/8pus/bad/undo_empty.8pus new file mode 100644 index 0000000..025c002 --- /dev/null +++ b/tests/8pus/bad/undo_empty.8pus @@ -0,0 +1 @@ +Undo. \ No newline at end of file diff --git a/tests/8pus/bad/undo_loop.8pus b/tests/8pus/bad/undo_loop.8pus new file mode 100644 index 0000000..c82db5e --- /dev/null +++ b/tests/8pus/bad/undo_loop.8pus @@ -0,0 +1,6 @@ +Goal A -> B. +intro. +Undo. +Undo. +Undo. +Undo. \ No newline at end of file diff --git a/tests/8pus/bad/undo_qed.8pus b/tests/8pus/bad/undo_qed.8pus new file mode 100644 index 0000000..5a58867 --- /dev/null +++ b/tests/8pus/bad/undo_qed.8pus @@ -0,0 +1,7 @@ +Goal (A -> B) -> A -> B. +intros. +apply H0. +exact H1. +Qed. +Undo. +Qed. \ No newline at end of file diff --git a/tests/8pus/bad/undo_try.8pus b/tests/8pus/bad/undo_try.8pus new file mode 100644 index 0000000..549111d --- /dev/null +++ b/tests/8pus/bad/undo_try.8pus @@ -0,0 +1,7 @@ +Goal A -> B -> A. +intros. +try intro. +Undo. +intro. +exact H0. +Qed. \ No newline at end of file diff --git a/tests/8pus/bad/unknown_tactic.8pus b/tests/8pus/bad/unknown_tactic.8pus new file mode 100644 index 0000000..d330417 --- /dev/null +++ b/tests/8pus/bad/unknown_tactic.8pus @@ -0,0 +1,2 @@ +Goal A -> B. +ancienttactic. \ No newline at end of file diff --git a/tests/8pus/bad/unkown_try.8pus b/tests/8pus/bad/unkown_try.8pus new file mode 100644 index 0000000..931350f --- /dev/null +++ b/tests/8pus/bad/unkown_try.8pus @@ -0,0 +1,3 @@ +Goal A -> B -> C -> A. +intros. +try autosolve. \ No newline at end of file