summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
Diffstat (limited to 'Test')
-rw-r--r--Test/absterm.art12
-rw-r--r--Test/absthm.art14
-rw-r--r--Test/appterm.art25
-rw-r--r--Test/appthm.art27
-rw-r--r--Test/assume.art8
-rw-r--r--Test/axiom.art9
-rw-r--r--Test/betaconv.art21
-rw-r--r--Test/cons.art4
-rw-r--r--Test/const.art2
-rw-r--r--Test/constterm.art7
-rw-r--r--Test/deductantisym.art13
-rw-r--r--Test/def.art6
-rw-r--r--Test/defineconst.art9
-rw-r--r--Test/definetypeop.art28
-rw-r--r--Test/eqmp.art37
-rw-r--r--Test/name.art1
-rw-r--r--Test/name2.art1
-rw-r--r--Test/nil.art1
-rw-r--r--Test/null.art0
-rw-r--r--Test/number.art1
-rw-r--r--Test/opType.art4
-rw-r--r--Test/pop.art2
-rw-r--r--Test/ref.art8
-rw-r--r--Test/refl.art6
-rw-r--r--Test/remove.art8
-rw-r--r--Test/subst.art47
-rw-r--r--Test/thm.art23
-rw-r--r--Test/timer.sh6
-rw-r--r--Test/typeop.art2
-rw-r--r--Test/var.art4
-rw-r--r--Test/varterm.art5
-rw-r--r--Test/vartype.art2
32 files changed, 0 insertions, 343 deletions
diff --git a/Test/absterm.art b/Test/absterm.art
deleted file mode 100644
index 94446fc..0000000
--- a/Test/absterm.art
+++ /dev/null
@@ -1,12 +0,0 @@
-"variablename"
-"variabletype"
-varType
-var
-"constname"
-const
-"consttype"
-typeOp
-nil
-opType
-constTerm
-absTerm
diff --git a/Test/absthm.art b/Test/absthm.art
deleted file mode 100644
index 359a4cd..0000000
--- a/Test/absthm.art
+++ /dev/null
@@ -1,14 +0,0 @@
-"bool"
-"bool"
-varType
-var
-#varTerm
-"bool"
-const
-"bool"
-typeOp
-nil
-opType
-constTerm
-refl
-absThm
diff --git a/Test/appterm.art b/Test/appterm.art
deleted file mode 100644
index 3d566c0..0000000
--- a/Test/appterm.art
+++ /dev/null
@@ -1,25 +0,0 @@
-"f"
-const
-"->"
-typeOp
-"bool"
-typeOp
-nil
-opType
-1
-def
-1
-remove
-nil
-cons
-cons
-opType
-constTerm
-"x"
-const
-"bool"
-typeOp
-nil
-opType
-constTerm
-appTerm
diff --git a/Test/appthm.art b/Test/appthm.art
deleted file mode 100644
index 7e54c8c..0000000
--- a/Test/appthm.art
+++ /dev/null
@@ -1,27 +0,0 @@
-"f"
-const
-"->"
-typeOp
-"bool"
-typeOp
-nil
-opType
-1
-def
-1
-remove
-nil
-cons
-cons
-opType
-constTerm
-refl
-"x"
-const
-"bool"
-typeOp
-nil
-opType
-constTerm
-refl
-appThm
diff --git a/Test/assume.art b/Test/assume.art
deleted file mode 100644
index ef47474..0000000
--- a/Test/assume.art
+++ /dev/null
@@ -1,8 +0,0 @@
-"bool"
-const
-"bool"
-typeOp
-nil
-opType
-constTerm
-assume
diff --git a/Test/axiom.art b/Test/axiom.art
deleted file mode 100644
index bcf79bf..0000000
--- a/Test/axiom.art
+++ /dev/null
@@ -1,9 +0,0 @@
-nil
-"name"
-const
-"bool"
-typeOp
-nil
-opType
-constTerm
-axiom
diff --git a/Test/betaconv.art b/Test/betaconv.art
deleted file mode 100644
index f0d051c..0000000
--- a/Test/betaconv.art
+++ /dev/null
@@ -1,21 +0,0 @@
-"x"
-"bool"
-typeOp
-nil
-opType
-1
-def
-var
-"c"
-const
-1
-ref
-constTerm
-absTerm
-"a"
-const
-1
-remove
-constTerm
-appTerm
-betaConv
diff --git a/Test/cons.art b/Test/cons.art
deleted file mode 100644
index b2c48b9..0000000
--- a/Test/cons.art
+++ /dev/null
@@ -1,4 +0,0 @@
-"bool"
-typeOp
-nil
-cons
diff --git a/Test/const.art b/Test/const.art
deleted file mode 100644
index 8a94755..0000000
--- a/Test/const.art
+++ /dev/null
@@ -1,2 +0,0 @@
-"name"
-const
diff --git a/Test/constterm.art b/Test/constterm.art
deleted file mode 100644
index ac94e2b..0000000
--- a/Test/constterm.art
+++ /dev/null
@@ -1,7 +0,0 @@
-"bool"
-const
-"bool"
-typeOp
-nil
-opType
-constTerm
diff --git a/Test/deductantisym.art b/Test/deductantisym.art
deleted file mode 100644
index 80a6eea..0000000
--- a/Test/deductantisym.art
+++ /dev/null
@@ -1,13 +0,0 @@
-"x"
-const
-"bool"
-typeOp
-nil
-opType
-constTerm
-assume
-1
-def
-1
-remove
-deductAntisym
diff --git a/Test/def.art b/Test/def.art
deleted file mode 100644
index 18cad67..0000000
--- a/Test/def.art
+++ /dev/null
@@ -1,6 +0,0 @@
-"bool"
-typeOp
-nil
-opType
-1
-def
diff --git a/Test/defineconst.art b/Test/defineconst.art
deleted file mode 100644
index 739f9c9..0000000
--- a/Test/defineconst.art
+++ /dev/null
@@ -1,9 +0,0 @@
-"y"
-"x"
-const
-"bool"
-typeOp
-nil
-opType
-constTerm
-defineConst
diff --git a/Test/definetypeop.art b/Test/definetypeop.art
deleted file mode 100644
index 706bd3e..0000000
--- a/Test/definetypeop.art
+++ /dev/null
@@ -1,28 +0,0 @@
-"n"
-"abs"
-"rep"
-"xtype"
-nil
-cons
-"x"
-"xtype"
-varType
-var
-"c"
-const
-"bool"
-typeOp
-nil
-opType
-1
-def
-constTerm
-absTerm
-"a"
-const
-1
-remove
-constTerm
-appTerm
-assume
-defineTypeOp
diff --git a/Test/eqmp.art b/Test/eqmp.art
deleted file mode 100644
index b7c63c6..0000000
--- a/Test/eqmp.art
+++ /dev/null
@@ -1,37 +0,0 @@
-"x"
-"bool"
-typeOp
-nil
-opType
-1
-def
-var
-"c"
-const
-1
-ref
-constTerm
-2
-def
-absTerm
-"a"
-const
-1
-ref
-constTerm
-3
-def
-appTerm
-refl
-"y"
-1
-remove
-var
-2
-remove
-absTerm
-3
-remove
-appTerm
-assume
-eqMp
diff --git a/Test/name.art b/Test/name.art
deleted file mode 100644
index bb89c74..0000000
--- a/Test/name.art
+++ /dev/null
@@ -1 +0,0 @@
-"bool"
diff --git a/Test/name2.art b/Test/name2.art
deleted file mode 100644
index a439e52..0000000
--- a/Test/name2.art
+++ /dev/null
@@ -1 +0,0 @@
-"->"
diff --git a/Test/nil.art b/Test/nil.art
deleted file mode 100644
index 607602c..0000000
--- a/Test/nil.art
+++ /dev/null
@@ -1 +0,0 @@
-nil
diff --git a/Test/null.art b/Test/null.art
deleted file mode 100644
index e69de29..0000000
--- a/Test/null.art
+++ /dev/null
diff --git a/Test/number.art b/Test/number.art
deleted file mode 100644
index f599e28..0000000
--- a/Test/number.art
+++ /dev/null
@@ -1 +0,0 @@
-10
diff --git a/Test/opType.art b/Test/opType.art
deleted file mode 100644
index 237dbd6..0000000
--- a/Test/opType.art
+++ /dev/null
@@ -1,4 +0,0 @@
-"name"
-typeOp
-nil
-opType
diff --git a/Test/pop.art b/Test/pop.art
deleted file mode 100644
index e111fc2..0000000
--- a/Test/pop.art
+++ /dev/null
@@ -1,2 +0,0 @@
-nil
-pop
diff --git a/Test/ref.art b/Test/ref.art
deleted file mode 100644
index acd59ea..0000000
--- a/Test/ref.art
+++ /dev/null
@@ -1,8 +0,0 @@
-"bool"
-typeOp
-nil
-opType
-1
-def
-1
-ref
diff --git a/Test/refl.art b/Test/refl.art
deleted file mode 100644
index 418ac89..0000000
--- a/Test/refl.art
+++ /dev/null
@@ -1,6 +0,0 @@
-"bool"
-"bool"
-varType
-var
-varTerm
-refl
diff --git a/Test/remove.art b/Test/remove.art
deleted file mode 100644
index 88cadad..0000000
--- a/Test/remove.art
+++ /dev/null
@@ -1,8 +0,0 @@
-"bool"
-typeOp
-nil
-opType
-1
-def
-1
-remove
diff --git a/Test/subst.art b/Test/subst.art
deleted file mode 100644
index 8fdc934..0000000
--- a/Test/subst.art
+++ /dev/null
@@ -1,47 +0,0 @@
-"ytype"
-"xtype"
-varType
-nil
-cons
-cons
-nil
-cons
-"y"
-"xtype"
-varType
-var
-"z"
-"xtype"
-varType
-var
-varTerm
-nil
-cons
-cons
-nil
-cons
-nil
-cons
-cons
-"y"
-"ytype"
-varType
-var
-"c"
-const
-"bool"
-typeOp
-nil
-opType
-1
-def
-constTerm
-absTerm
-"a"
-const
-1
-remove
-constTerm
-appTerm
-assume
-subst
diff --git a/Test/thm.art b/Test/thm.art
deleted file mode 100644
index 4fee8b2..0000000
--- a/Test/thm.art
+++ /dev/null
@@ -1,23 +0,0 @@
-"x"
-"bool"
-typeOp
-nil
-opType
-1
-def
-var
-varTerm
-assume
-"y"
-1
-ref
-var
-varTerm
-nil
-cons
-"z"
-1
-remove
-var
-varTerm
-thm
diff --git a/Test/timer.sh b/Test/timer.sh
deleted file mode 100644
index 2a1e7c3..0000000
--- a/Test/timer.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-#!/bin/bash
-
-for i in {1..1}
-do
- $1 $2 > /dev/null
-done
diff --git a/Test/typeop.art b/Test/typeop.art
deleted file mode 100644
index 6b85dd7..0000000
--- a/Test/typeop.art
+++ /dev/null
@@ -1,2 +0,0 @@
-"bool"
-typeOp
diff --git a/Test/var.art b/Test/var.art
deleted file mode 100644
index 4c915e7..0000000
--- a/Test/var.art
+++ /dev/null
@@ -1,4 +0,0 @@
-"bool"
-"bool"
-varType
-var
diff --git a/Test/varterm.art b/Test/varterm.art
deleted file mode 100644
index 5bbc768..0000000
--- a/Test/varterm.art
+++ /dev/null
@@ -1,5 +0,0 @@
-"bool"
-"bool"
-varType
-var
-varTerm
diff --git a/Test/vartype.art b/Test/vartype.art
deleted file mode 100644
index 72e6b3c..0000000
--- a/Test/vartype.art
+++ /dev/null
@@ -1,2 +0,0 @@
-"bool"
-varType