From 5395287cc2f758d94bec8befe8956ba2dcc3940c Mon Sep 17 00:00:00 2001 From: Jed Barber Date: Thu, 15 Dec 2016 14:28:31 +1100 Subject: Old uncommitted changes --- test/absthm.art | 28 +++++++-------- test/appterm.art | 50 +++++++++++++-------------- test/appthm.art | 54 ++++++++++++++--------------- test/assume.art | 16 ++++----- test/axiom.art | 18 +++++----- test/betaconv.art | 42 +++++++++++----------- test/cons.art | 8 ++--- test/const.art | 4 +-- test/constterm.art | 14 ++++---- test/deductantisym.art | 26 +++++++------- test/def.art | 12 +++---- test/defineconst.art | 18 +++++----- test/definetypeop.art | 56 +++++++++++++++--------------- test/eqmp.art | 74 +++++++++++++++++++-------------------- test/name2.art | 2 +- test/nil.art | 2 +- test/number.art | 2 +- test/opType.art | 8 ++--- test/pop.art | 4 +-- test/ref.art | 16 ++++----- test/refl.art | 12 +++---- test/remove.art | 16 ++++----- test/subst.art | 94 +++++++++++++++++++++++++------------------------- test/thm.art | 46 ++++++++++++------------ test/typeop.art | 4 +-- test/var.art | 8 ++--- test/varterm.art | 10 +++--- test/vartype.art | 4 +-- 28 files changed, 324 insertions(+), 324 deletions(-) (limited to 'test') 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 -- cgit