diff --git a/tests/and.8pus b/tests/and.8pus new file mode 100644 index 0000000..b323ca4 --- /dev/null +++ b/tests/and.8pus @@ -0,0 +1,6 @@ +Goal A -> B -> (A /\ B). +intros. +split. + exact H0. + exact H1. +Qed. diff --git a/tests/exact.8pus b/tests/exact.8pus new file mode 100644 index 0000000..fc691ca --- /dev/null +++ b/tests/exact.8pus @@ -0,0 +1,4 @@ +Goal A -> B -> A. +intros. + exact H0. +Qed. diff --git a/tests/or.8pus b/tests/or.8pus new file mode 100644 index 0000000..982cb82 --- /dev/null +++ b/tests/or.8pus @@ -0,0 +1,5 @@ +Goal A -> B -> (A \/ C). +intros. +left. +exact H0. +Qed.