Include Church factorial samples

codedot · codedot · commit e15c8b2b1a03 · 2017-01-31T15:44:20.000+02:00
diff --git a/samples/cfact4.mlc b/samples/cfact4.mlc
@@ -0,0 +1,3 @@
+FACT = n: n (p, q: MULT q (p (SUCC q))) (p: C1) C1;
+
+MINUS (C3 C3) (FACT C4)
diff --git a/samples/cfact5.mlc b/samples/cfact5.mlc
@@ -0,0 +1,3 @@
+FACT = n: n (p, q: MULT q (p (SUCC q))) (p: C1) C1;
+
+MINUS (C3 C5) (FACT C5)
diff --git a/test.sh b/test.sh
@@ -42,8 +42,14 @@ compare w2eta "v1, v2: v1 (v1 (v1 (v1 v2)))" \
 compare 1022ii "v1: v1" \
 	ABSTRACT closed NORMAL OPTIMAL TURNING
 
+compare cfact4 "v1, v2: v1 (v1 (v1 v2))" \
+	abstract closed normal optimal turning
+
 compare yfact4 "v1, v2: v1 (v1 (v1 v2))" \
 	abstract closed normal optimal turning
 
+compare cfact5 "v1, v2: v1 (v1 (v1 (v1 (v1 v2))))" \
+	abstract closed normal optimal turning
+
 compare yfact5 "v1, v2: v1 (v1 (v1 (v1 (v1 v2))))" \
 	abstract closed normal OPTIMAL turning
