summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
authorJed Barber <jjbarber@y7mail.com>2016-12-15 14:28:31 +1100
committerJed Barber <jjbarber@y7mail.com>2016-12-15 14:28:31 +1100
commit5395287cc2f758d94bec8befe8956ba2dcc3940c (patch)
treefca41713cd7f8a27d41ba0d186adc1e616cf447b /test
parent2fc745bef05860e16a2e89e465a30dc59b5ec2e5 (diff)
Old uncommitted changes
Diffstat (limited to 'test')
-rw-r--r--test/absthm.art28
-rw-r--r--test/appterm.art50
-rw-r--r--test/appthm.art54
-rw-r--r--test/assume.art16
-rw-r--r--test/axiom.art18
-rw-r--r--test/betaconv.art42
-rw-r--r--test/cons.art8
-rw-r--r--test/const.art4
-rw-r--r--test/constterm.art14
-rw-r--r--test/deductantisym.art26
-rw-r--r--test/def.art12
-rw-r--r--test/defineconst.art18
-rw-r--r--test/definetypeop.art56
-rw-r--r--test/eqmp.art74
-rw-r--r--test/name2.art2
-rw-r--r--test/nil.art2
-rw-r--r--test/number.art2
-rw-r--r--test/opType.art8
-rw-r--r--test/pop.art4
-rw-r--r--test/ref.art16
-rw-r--r--test/refl.art12
-rw-r--r--test/remove.art16
-rw-r--r--test/subst.art94
-rw-r--r--test/thm.art46
-rw-r--r--test/typeop.art4
-rw-r--r--test/var.art8
-rw-r--r--test/varterm.art10
-rw-r--r--test/vartype.art4
28 files changed, 324 insertions, 324 deletions
diff --git a/test/absthm.art b/test/absthm.art
index 359a4cd..244f89a 100644
--- a/test/absthm.art
+++ b/test/absthm.art
@@ -1,14 +1,14 @@
-"bool"
-"bool"
-varType
-var
-#varTerm
-"bool"
-const
-"bool"
-typeOp
-nil
-opType
-constTerm
-refl
-absThm
+"bool"
+"bool"
+varType
+var
+#varTerm
+"bool"
+const
+"bool"
+typeOp
+nil
+opType
+constTerm
+refl
+absThm
diff --git a/test/appterm.art b/test/appterm.art
index 3d566c0..5e5763f 100644
--- a/test/appterm.art
+++ b/test/appterm.art
@@ -1,25 +1,25 @@
-"f"
-const
-"->"
-typeOp
-"bool"
-typeOp
-nil
-opType
-1
-def
-1
-remove
-nil
-cons
-cons
-opType
-constTerm
-"x"
-const
-"bool"
-typeOp
-nil
-opType
-constTerm
-appTerm
+"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
index 7e54c8c..c6e0787 100644
--- a/test/appthm.art
+++ b/test/appthm.art
@@ -1,27 +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
+"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
index ef47474..2d6e097 100644
--- a/test/assume.art
+++ b/test/assume.art
@@ -1,8 +1,8 @@
-"bool"
-const
-"bool"
-typeOp
-nil
-opType
-constTerm
-assume
+"bool"
+const
+"bool"
+typeOp
+nil
+opType
+constTerm
+assume
diff --git a/test/axiom.art b/test/axiom.art
index bcf79bf..5940bc6 100644
--- a/test/axiom.art
+++ b/test/axiom.art
@@ -1,9 +1,9 @@
-nil
-"name"
-const
-"bool"
-typeOp
-nil
-opType
-constTerm
-axiom
+nil
+"name"
+const
+"bool"
+typeOp
+nil
+opType
+constTerm
+axiom
diff --git a/test/betaconv.art b/test/betaconv.art
index f0d051c..a4166bd 100644
--- a/test/betaconv.art
+++ b/test/betaconv.art
@@ -1,21 +1,21 @@
-"x"
-"bool"
-typeOp
-nil
-opType
-1
-def
-var
-"c"
-const
-1
-ref
-constTerm
-absTerm
-"a"
-const
-1
-remove
-constTerm
-appTerm
-betaConv
+"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
index b2c48b9..da46e33 100644
--- a/test/cons.art
+++ b/test/cons.art
@@ -1,4 +1,4 @@
-"bool"
-typeOp
-nil
-cons
+"bool"
+typeOp
+nil
+cons
diff --git a/test/const.art b/test/const.art
index 8a94755..bc2d1c9 100644
--- a/test/const.art
+++ b/test/const.art
@@ -1,2 +1,2 @@
-"name"
-const
+"name"
+const
diff --git a/test/constterm.art b/test/constterm.art
index ac94e2b..cacb07d 100644
--- a/test/constterm.art
+++ b/test/constterm.art
@@ -1,7 +1,7 @@
-"bool"
-const
-"bool"
-typeOp
-nil
-opType
-constTerm
+"bool"
+const
+"bool"
+typeOp
+nil
+opType
+constTerm
diff --git a/test/deductantisym.art b/test/deductantisym.art
index 80a6eea..d61b22e 100644
--- a/test/deductantisym.art
+++ b/test/deductantisym.art
@@ -1,13 +1,13 @@
-"x"
-const
-"bool"
-typeOp
-nil
-opType
-constTerm
-assume
-1
-def
-1
-remove
-deductAntisym
+"x"
+const
+"bool"
+typeOp
+nil
+opType
+constTerm
+assume
+1
+def
+1
+remove
+deductAntisym
diff --git a/test/def.art b/test/def.art
index 18cad67..7595e27 100644
--- a/test/def.art
+++ b/test/def.art
@@ -1,6 +1,6 @@
-"bool"
-typeOp
-nil
-opType
-1
-def
+"bool"
+typeOp
+nil
+opType
+1
+def
diff --git a/test/defineconst.art b/test/defineconst.art
index 739f9c9..79ab9b3 100644
--- a/test/defineconst.art
+++ b/test/defineconst.art
@@ -1,9 +1,9 @@
-"y"
-"x"
-const
-"bool"
-typeOp
-nil
-opType
-constTerm
-defineConst
+"y"
+"x"
+const
+"bool"
+typeOp
+nil
+opType
+constTerm
+defineConst
diff --git a/test/definetypeop.art b/test/definetypeop.art
index 706bd3e..5577613 100644
--- a/test/definetypeop.art
+++ b/test/definetypeop.art
@@ -1,28 +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
+"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
index b7c63c6..bafbea9 100644
--- a/test/eqmp.art
+++ b/test/eqmp.art
@@ -1,37 +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
+"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/name2.art b/test/name2.art
index a439e52..f62bdc2 100644
--- a/test/name2.art
+++ b/test/name2.art
@@ -1 +1 @@
-"->"
+"->"
diff --git a/test/nil.art b/test/nil.art
index 607602c..9b021e8 100644
--- a/test/nil.art
+++ b/test/nil.art
@@ -1 +1 @@
-nil
+nil
diff --git a/test/number.art b/test/number.art
index f599e28..d434014 100644
--- a/test/number.art
+++ b/test/number.art
@@ -1 +1 @@
-10
+10
diff --git a/test/opType.art b/test/opType.art
index 237dbd6..8548457 100644
--- a/test/opType.art
+++ b/test/opType.art
@@ -1,4 +1,4 @@
-"name"
-typeOp
-nil
-opType
+"name"
+typeOp
+nil
+opType
diff --git a/test/pop.art b/test/pop.art
index e111fc2..3717446 100644
--- a/test/pop.art
+++ b/test/pop.art
@@ -1,2 +1,2 @@
-nil
-pop
+nil
+pop
diff --git a/test/ref.art b/test/ref.art
index acd59ea..2042b3e 100644
--- a/test/ref.art
+++ b/test/ref.art
@@ -1,8 +1,8 @@
-"bool"
-typeOp
-nil
-opType
-1
-def
-1
-ref
+"bool"
+typeOp
+nil
+opType
+1
+def
+1
+ref
diff --git a/test/refl.art b/test/refl.art
index 418ac89..3e8e20e 100644
--- a/test/refl.art
+++ b/test/refl.art
@@ -1,6 +1,6 @@
-"bool"
-"bool"
-varType
-var
-varTerm
-refl
+"bool"
+"bool"
+varType
+var
+varTerm
+refl
diff --git a/test/remove.art b/test/remove.art
index 88cadad..4f82808 100644
--- a/test/remove.art
+++ b/test/remove.art
@@ -1,8 +1,8 @@
-"bool"
-typeOp
-nil
-opType
-1
-def
-1
-remove
+"bool"
+typeOp
+nil
+opType
+1
+def
+1
+remove
diff --git a/test/subst.art b/test/subst.art
index 8fdc934..c46903e 100644
--- a/test/subst.art
+++ b/test/subst.art
@@ -1,47 +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
+"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
index 4fee8b2..4ce6a1c 100644
--- a/test/thm.art
+++ b/test/thm.art
@@ -1,23 +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
+"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/typeop.art b/test/typeop.art
index 6b85dd7..5a6abaf 100644
--- a/test/typeop.art
+++ b/test/typeop.art
@@ -1,2 +1,2 @@
-"bool"
-typeOp
+"bool"
+typeOp
diff --git a/test/var.art b/test/var.art
index 4c915e7..6dc6a0f 100644
--- a/test/var.art
+++ b/test/var.art
@@ -1,4 +1,4 @@
-"bool"
-"bool"
-varType
-var
+"bool"
+"bool"
+varType
+var
diff --git a/test/varterm.art b/test/varterm.art
index 5bbc768..3a2b04f 100644
--- a/test/varterm.art
+++ b/test/varterm.art
@@ -1,5 +1,5 @@
-"bool"
-"bool"
-varType
-var
-varTerm
+"bool"
+"bool"
+varType
+var
+varTerm
diff --git a/test/vartype.art b/test/vartype.art
index 72e6b3c..c9a5e7a 100644
--- a/test/vartype.art
+++ b/test/vartype.art
@@ -1,2 +1,2 @@
-"bool"
-varType
+"bool"
+varType