From b4ba9432cdcc56d55559ed8b18bb1cf15714e850 Mon Sep 17 00:00:00 2001 From: augustin64 Date: Tue, 14 May 2024 15:23:58 +0200 Subject: [PATCH] Add a few tests --- tests/and.8pus | 6 ++++++ tests/exact.8pus | 4 ++++ tests/or.8pus | 5 +++++ 3 files changed, 15 insertions(+) create mode 100644 tests/and.8pus create mode 100644 tests/exact.8pus create mode 100644 tests/or.8pus 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.