removed transfer from gf3

1 files changed, 0 insertions, 94 deletions

diff --git a/transfer/examples/numerals.tra b/transfer/examples/numerals.tra
deleted file mode 100644
index 2c2718130..000000000
--- a/transfer/examples/numerals.tra
+++ /dev/null
@@ -1,94 +0,0 @@
-import prelude
-
-data Cat : Type where {
-  Digit : Cat ;
-  Numeral : Cat ;
-  Sub10 : Cat ;
-  Sub100 : Cat ;
-  Sub1000 : Cat ;
-  Sub1000000 : Cat
-} ;
-
-data Tree : (_ : Cat)-> Type where {
-  n2 : Tree Digit ;
-  n3 : Tree Digit ;
-  n4 : Tree Digit ;
-  n5 : Tree Digit ;
-  n6 : Tree Digit ;
-  n7 : Tree Digit ;
-  n8 : Tree Digit ;
-  n9 : Tree Digit ;
-  num : (_ : Tree Sub1000000)-> Tree Numeral ;
-  pot0 : (_ : Tree Digit)-> Tree Sub10 ;
-  pot01 : Tree Sub10 ;
-  pot0as1 : (_ : Tree Sub10)-> Tree Sub100 ;
-  pot1 : (_ : Tree Digit)-> Tree Sub100 ;
-  pot110 : Tree Sub100 ;
-  pot111 : Tree Sub100 ;
-  pot1as2 : (_ : Tree Sub100)-> Tree Sub1000 ;
-  pot1plus : (_ : Tree Digit)-> (_ : Tree Sub10)-> Tree Sub100 ;
-  pot1to19 : (_ : Tree Digit)-> Tree Sub100 ;
-  pot2 : (_ : Tree Sub10)-> Tree Sub1000 ;
-  pot2as3 : (_ : Tree Sub1000)-> Tree Sub1000000 ;
-  pot2plus : (_ : Tree Sub10)-> (_ : Tree Sub100)-> Tree Sub1000 ;
-  pot3 : (_ : Tree Sub1000)-> Tree Sub1000000 ;
-  pot3plus : (_ : Tree Sub1000)-> (_ : Tree Sub1000)-> Tree Sub1000000
-}
-
-derive Compos Tree
-
-
-data Binary_Cat : Type where {
-  Bin : Binary_Cat
-} ;
-data Binary_Tree : (_ : Binary_Cat)-> Type where {
-  End : Binary_Tree Bin ;
-  One : (_ : Binary_Tree Bin)-> Binary_Tree Bin ;
-  Zero : (_ : Binary_Tree Bin)-> Binary_Tree Bin
-}
-
-
-
-monoid_plus_Int : Monoid Integer
-monoid_plus_Int = rec mzero = 0
-		      mplus = (\x -> \y -> x + y)
-
-
-num2int : Tree Numeral -> Integer
-num2int = tree2int ?
-
-tree2int : (C : Cat) -> Tree C -> Integer 
-tree2int _ n = case n of
-		n2 -> 2
-		n3 -> 3
-		n4 -> 4
-		n5 -> 5
-		n6 -> 6
-		n7 -> 7
-		n8 -> 8
-		n9 -> 9
-		pot01 -> 1
-		pot1 x -> 10 * tree2int ? x
-		pot110 -> 10
-		pot111 -> 11
-		pot1plus x y -> 10 * tree2int ? x + tree2int ? y
-		pot1to19 x -> 10 + tree2int ? x
-		pot2 x -> 100 * tree2int ? x
-		pot2as3 x -> 10 * tree2int ? x
-		pot2plus x y -> 100 * tree2int ? x + tree2int ? y
-		pot3 x -> 1000 * tree2int ? x
-		pot3plus x y -> 1000 * tree2int ? x + tree2int ? y
-                _ -> composFold ? ? compos_Tree ? monoid_plus_Int C tree2int n
-
-int2bin : Integer -> Binary_Tree Bin
-int2bin = int2bin_ End
-
-int2bin_ : Binary_Tree Bin -> Integer -> Binary_Tree Bin
-int2bin_ b 0 = b
-int2bin_ b n = let d = if n % 2 == 0 then Zero else One
-		   q = n / 2
-                in int2bin_ (d b) q
-
-num2bin : Tree Numeral -> Binary_Tree Bin
-num2bin n = int2bin (num2int n)
-