The rest of the article files for testing specific commands

13 files changed, 215 insertions, 11 deletions

diff --git a/Test/absterm.art b/Test/absterm.art
index d68ddc6..94446fc 100644
--- a/Test/absterm.art
+++ b/Test/absterm.art
@@ -1,11 +1,10 @@
-"bool"
-"bool"
+"variablename"
+"variabletype"
 varType
 var
-varTerm
-"bool"
+"constname"
 const
-"bool"
+"consttype"
 typeOp
 nil
 opType
diff --git a/Test/absthm.art b/Test/absthm.art
index 6fd12ba..359a4cd 100644
--- a/Test/absthm.art
+++ b/Test/absthm.art
@@ -1,8 +1,8 @@
 "bool"
 "bool"
-var
 varType
-varTerm
+var
+#varTerm
 "bool"
 const
 "bool"
diff --git a/Test/appterm.art b/Test/appterm.art
index 42f0da9..3d566c0 100644
--- a/Test/appterm.art
+++ b/Test/appterm.art
@@ -1,4 +1,4 @@
-"name"
+"f"
 const
 "->"
 typeOp
@@ -15,7 +15,7 @@ cons
 cons
 opType
 constTerm
-"name"
+"x"
 const
 "bool"
 typeOp
diff --git a/Test/appthm.art b/Test/appthm.art
new file mode 100644
index 0000000..7e54c8c
--- /dev/null
+++ b/Test/appthm.art
@@ -0,0 +1,27 @@
+"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/betaconv.art b/Test/betaconv.art
new file mode 100644
index 0000000..f0d051c
--- /dev/null
+++ b/Test/betaconv.art
@@ -0,0 +1,21 @@
+"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/deductantisym.art b/Test/deductantisym.art
new file mode 100644
index 0000000..80a6eea
--- /dev/null
+++ b/Test/deductantisym.art
@@ -0,0 +1,13 @@
+"x"
+const
+"bool"
+typeOp
+nil
+opType
+constTerm
+assume
+1
+def
+1
+remove
+deductAntisym
diff --git a/Test/defineconst.art b/Test/defineconst.art
new file mode 100644
index 0000000..739f9c9
--- /dev/null
+++ b/Test/defineconst.art
@@ -0,0 +1,9 @@
+"y"
+"x"
+const
+"bool"
+typeOp
+nil
+opType
+constTerm
+defineConst
diff --git a/Test/definetypeop.art b/Test/definetypeop.art
new file mode 100644
index 0000000..706bd3e
--- /dev/null
+++ b/Test/definetypeop.art
@@ -0,0 +1,28 @@
+"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
new file mode 100644
index 0000000..b7c63c6
--- /dev/null
+++ b/Test/eqmp.art
@@ -0,0 +1,37 @@
+"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/null.art b/Test/null.art
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/Test/null.art
diff --git a/Test/subst.art b/Test/subst.art
new file mode 100644
index 0000000..8fdc934
--- /dev/null
+++ b/Test/subst.art
@@ -0,0 +1,47 @@
+"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
new file mode 100644
index 0000000..4fee8b2
--- /dev/null
+++ b/Test/thm.art
@@ -0,0 +1,23 @@
+"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
index 637b80a..c95aff5 100644
--- a/Test/timer.sh
+++ b/Test/timer.sh
@@ -1,6 +1,6 @@
 #!/bin/bash
 
-for i in (1..1000)
+for i in {1..1000}
 do
-  $1 $2
+  $1 $2 > /dev/null
 done