From 02c45922fc897047ecce16cc02398338947e7b94 Mon Sep 17 00:00:00 2001
From: Camil Staps
Date: Fri, 3 Jul 2015 11:16:02 +0200
Subject: Fix associativity

---
 LogicTest.icl | 33 +++++++++++++++++++++++++++++++++
 1 file changed, 33 insertions(+)
 create mode 100644 LogicTest.icl

(limited to 'LogicTest.icl')

diff --git a/LogicTest.icl b/LogicTest.icl
new file mode 100644
index 0000000..69adc8a
--- /dev/null
+++ b/LogicTest.icl
@@ -0,0 +1,33 @@
+module LogicTest
+
+import Logic
+
+// Some random examples
+e1 = Atom 'p'
+e2 = Atom 'q'
+e3 = App1 Not e1
+e4 = App2 e1 And e2
+e5 = App2 e3 Or e2
+e6 = App2 e3 Impl e3
+e7 = App2 e4 Equiv e5
+e8 = App2 (App2 (Atom 'p') And (Atom 'q')) Impl (Atom 'q')
+e9 = App2 (Atom 'p') And (App2 (Atom 'q') Impl (Atom 'q'))
+
+exprs_rand = [e1,e2,e3,e4,e5,e6,e7,e8,e9]
+
+// To test associativity rules
+e10 = App2 (App2 (Atom 'p') And (Atom 'q')) And (Atom 'r')
+e11 = App2 (Atom 'p') And (App2 (Atom 'q') And (Atom 'r'))
+
+e12 = App2 (App2 (Atom 'p') Or (Atom 'q')) Or (Atom 'r')
+e13 = App2 (Atom 'p') Or (App2 (Atom 'q') Or (Atom 'r'))
+
+e14 = App2 (App2 (Atom 'p') Impl (Atom 'q')) Impl (Atom 'r')
+e15 = App2 (Atom 'p') Impl (App2 (Atom 'q') Impl (Atom 'r'))
+
+e16 = App2 (App2 (Atom 'p') Equiv (Atom 'q')) Equiv (Atom 'r')
+e17 = App2 (Atom 'p') Equiv (App2 (Atom 'q') Equiv (Atom 'r'))
+
+exprs_assoc = [e10,e11,e12,e13,e14,e15,e16,e17]
+
+Start = map toString exprs_assoc
-- 
cgit v1.2.3