diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/absthm.art | 28 | ||||
| -rw-r--r-- | test/appterm.art | 50 | ||||
| -rw-r--r-- | test/appthm.art | 54 | ||||
| -rw-r--r-- | test/assume.art | 16 | ||||
| -rw-r--r-- | test/axiom.art | 18 | ||||
| -rw-r--r-- | test/betaconv.art | 42 | ||||
| -rw-r--r-- | test/cons.art | 8 | ||||
| -rw-r--r-- | test/const.art | 4 | ||||
| -rw-r--r-- | test/constterm.art | 14 | ||||
| -rw-r--r-- | test/deductantisym.art | 26 | ||||
| -rw-r--r-- | test/def.art | 12 | ||||
| -rw-r--r-- | test/defineconst.art | 18 | ||||
| -rw-r--r-- | test/definetypeop.art | 56 | ||||
| -rw-r--r-- | test/eqmp.art | 74 | ||||
| -rw-r--r-- | test/name2.art | 2 | ||||
| -rw-r--r-- | test/nil.art | 2 | ||||
| -rw-r--r-- | test/number.art | 2 | ||||
| -rw-r--r-- | test/opType.art | 8 | ||||
| -rw-r--r-- | test/pop.art | 4 | ||||
| -rw-r--r-- | test/ref.art | 16 | ||||
| -rw-r--r-- | test/refl.art | 12 | ||||
| -rw-r--r-- | test/remove.art | 16 | ||||
| -rw-r--r-- | test/subst.art | 94 | ||||
| -rw-r--r-- | test/thm.art | 46 | ||||
| -rw-r--r-- | test/typeop.art | 4 | ||||
| -rw-r--r-- | test/var.art | 8 | ||||
| -rw-r--r-- | test/varterm.art | 10 | ||||
| -rw-r--r-- | test/vartype.art | 4 |
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
|