removed transfer from gf3

18 files changed, 0 insertions, 724 deletions

diff --git a/transfer/examples/aggregation/Abstract.gf b/transfer/examples/aggregation/Abstract.gf
deleted file mode 100644
index 9d8b31d0d..000000000
--- a/transfer/examples/aggregation/Abstract.gf
+++ /dev/null
@@ -1,24 +0,0 @@
--- testing transfer: aggregation by def definitions. AR 12/4/2003 -- 9/10
-
---   p "Mary runs or John runs and John walks" | l -transfer=Aggregation
---   Mary runs or John runs and walks
---   Mary or John runs and John walks
-
--- The two results are due to ambiguity in parsing. Thus it is not spurious!
-
-abstract Abstract = {
-
-cat 
-  S ; NP ; VP ; Conj ;
-
-fun
-  Pred : NP -> VP -> S ;
-  ConjS : Conj -> S -> S -> S ;
-  ConjVP : Conj -> VP -> VP -> VP ;
-  ConjNP : Conj -> NP -> NP -> NP ;
-
-  John, Mary, Bill : NP ;
-  Walk, Run, Swim : VP ;
-  And, Or : Conj ;
-
-}
diff --git a/transfer/examples/aggregation/English.gf b/transfer/examples/aggregation/English.gf
deleted file mode 100644
index 53199787b..000000000
--- a/transfer/examples/aggregation/English.gf
+++ /dev/null
@@ -1,41 +0,0 @@
-concrete English of Abstract = {
-
-lincat 
-  VP = {s : Num => Str} ;
-  NP, Conj = {s : Str ; n : Num} ;
-
-lin
-  Pred np vp = ss (np.s ++ vp.s ! np.n) ;
-  ConjS c A  B = ss (A.s ++ c.s ++ B.s) ;
-  ConjVP c A  B = {s = \\n => A.s ! n ++ c.s ++ B.s ! n} ;
-  ConjNP c A  B = {s = A.s ++ c.s ++ B.s ; n = c.n} ;
-  
-  John = pn "John" ;
-  Mary = pn "Mary" ;
-  Bill = pn "Bill" ;
-  Walk = vp "walk" ;
-  Run  = vp "run" ;
-  Swim = vp "swim" ;
-
-  And = {s = "and" ; n = Pl} ;
-  Or = pn "or" ;
-
-param
-  Num = Sg | Pl ;
-
-oper
-  vp : Str -> {s : Num => Str} = \run -> {
-    s = table {
-      Sg => run + "s" ;
-      Pl => run
-      }
-    } ;
-
-  pn : Str -> {s : Str ; n : Num} = \bob -> {
-    s = bob ;
-    n = Sg
-    } ;
-
-  ss : Str -> {s : Str} = \s -> {s = s} ;
-
-}
diff --git a/transfer/examples/aggregation/aggregate.tra b/transfer/examples/aggregation/aggregate.tra
deleted file mode 100644
index b71ccfef2..000000000
--- a/transfer/examples/aggregation/aggregate.tra
+++ /dev/null
@@ -1,56 +0,0 @@
-import prelude
-import tree
-
-
--- aggreg specialized for Tree S
-aggregS : Tree S -> Tree S
-aggregS = aggreg S
-
--- For now, here's what we have to do:
-aggreg : (A : Type) -> Tree A -> Tree A
-aggreg _ t = 
-  case t of
-      ConjS c s1 s2 -> 
-	case (aggreg ? s1, aggreg ? s2) of
-	     (Pred np1 vp1, Pred np2 vp2) | eq NP (eq_Tree NP) np1 np2 -> 
-			Pred np1 (ConjVP c vp1 vp2)
-             (Pred np1 vp1, Pred np2 vp2) | eq VP (eq_Tree VP) vp1 vp2 -> 
-	        	Pred (ConjNP c np1 np2) vp1
-	     (s1',s2') -> ConjS c s1' s2'
-      _ -> composOp ? ? compos_Tree ? aggreg t
-
-
-
-
-
-{-
--- When the Transfer compiler gets meta variable inference,
--- we can write this:
-aggreg : (A : Type) -> Tree A -> Tree A
-aggreg _ t = 
-  case t of
-      ConjS c s1 s2 -> 
-	case (aggreg ? s1, aggreg ? s2) of
-		(Pred np1 vp1, Pred np2 vp2) | np1 == np2 -> 
-			Pred np1 (ConjVP c vp1 vp2)
-                (Pred np1 vp1, Pred np2 vp2) | vp1 == vp2 -> 
-	        	Pred (ConjNP c np1 np2) vp1
-		(s1',s2') -> ConjS c s1' s2'
-      _ -> composOp ? ? ? ? aggreg t
--}
-
-
-{-
--- If we added idden arguments, we could write something like this:
-aggreg : (A : Type) => Tree A -> Tree A
-aggreg t = 
-  case t of
-      ConjS c s1 s2 -> 
-	case (aggreg s1, aggreg s2) of
-		(Pred np1 vp1, Pred np2 vp2) | np1 == np2 -> 
-			Pred np1 (ConjVP c vp1 vp2)
-                (Pred np1 vp1, Pred np2 vp2) | vp1 == vp2 -> 
-	        	Pred (ConjNP c np1 np2) vp1
-		(s1',s2') -> ConjS c s1' s2'
-      _ -> composOp aggreg t
--}
diff --git a/transfer/examples/aggregation/tree.tra b/transfer/examples/aggregation/tree.tra
deleted file mode 100644
index 5515efa21..000000000
--- a/transfer/examples/aggregation/tree.tra
+++ /dev/null
@@ -1,23 +0,0 @@
-import prelude ;
-data Cat : Type where {
-  Conj : Cat ;
-  NP : Cat ;
-  S : Cat ;
-  VP : Cat 
-} ;
-data Tree : Cat -> Type where {
-  And : Tree Conj ;
-  Bill : Tree NP ;
-  ConjNP : Tree Conj -> Tree NP -> Tree NP -> Tree NP ;
-  ConjS : Tree Conj -> Tree S -> Tree S -> Tree S ;
-  ConjVP : Tree Conj -> Tree VP -> Tree VP -> Tree VP ;
-  John : Tree NP ;
-  Mary : Tree NP ;
-  Or : Tree Conj ;
-  Pred : Tree NP -> Tree VP -> Tree S ;
-  Run : Tree VP ;
-  Swim : Tree VP ;
-  Walk : Tree VP 
-} ;
-derive Eq Tree ;
-derive Compos Tree ;
diff --git a/transfer/examples/disjpatt.tra b/transfer/examples/disjpatt.tra
deleted file mode 100644
index 740e08a7b..000000000
--- a/transfer/examples/disjpatt.tra
+++ /dev/null
@@ -1,24 +0,0 @@
-data Cat : Type where
-    VarOrWild : Cat
-    Exp : Cat
-    Ident : Cat
-
-data Tree : Cat -> Type where
-    EAbs : Tree VarOrWild -> Tree Exp -> Tree Exp
-    EPi : Tree VarOrWild -> Tree Exp -> Tree Exp -> Tree Exp
-    EVar : Tree Ident -> Tree Exp
-    EType : Tree Exp
-    EStr : String -> Tree Exp
-    EInt : Integer -> Tree Exp
-    VVar : Tree Ident -> Tree VarOrWild
-    VWild : Tree VarOrWild
-    Ident : String -> Tree Ident
-
-
-f e = case e of
-       EAbs (VWild || VVar _) e || EPi (VWild || VVar _) _ e -> doSomething e
-       Ident i -> Ident i
-       _ -> catchAll
-
-
-g (Ident x || EAbs (VWild || VVar _) t e) = x e
\ No newline at end of file
diff --git a/transfer/examples/exp.tra b/transfer/examples/exp.tra
deleted file mode 100644
index e54b82055..000000000
--- a/transfer/examples/exp.tra
+++ /dev/null
@@ -1,33 +0,0 @@
-import prelude
-
-data Cat : Type where
-  Stm : Cat
-  Exp : Cat
-  Var : Cat
-  Typ : Cat
-  ListStm : Cat
-
-data Tree : Cat -> Type where
-  SDecl   : Tree Typ -> Tree Var -> Tree Stm
-  SAss    : Tree Var -> Tree Exp -> Tree Stm
-  SBlock  : Tree ListStm -> Tree Stm
-  EAdd    : Tree Exp -> Tree Exp -> Tree Exp
-  EStm    : Tree Stm -> Tree Exp
-  EVar    : Tree Var -> Tree Exp
-  EInt    : Integer -> Tree Exp
-  V       : String -> Tree Var
-  TInt    : Tree Typ
-  TFloat  : Tree Typ
-
-  NilStm  : Tree ListStm
-  ConsStm : Tree Stm -> Tree ListStm -> Tree ListStm
-
-derive Compos Tree
-
-rename : (String -> String) -> (C : Type) -> Tree C -> Tree C
-rename f C t = case t of
-		   V x -> V (f x)
-		   _ -> composOp ? ? compos_Tree C (rename f) t
-
-
-main = rename (const ? ? "apa") Stm (SAss (V "y") (EAdd (EVar (V "x")) (EInt 2)))
\ No newline at end of file
diff --git a/transfer/examples/fib.tra b/transfer/examples/fib.tra
deleted file mode 100644
index 43e533b1f..000000000
--- a/transfer/examples/fib.tra
+++ /dev/null
@@ -1,12 +0,0 @@
-import nat
-import prelude
-
-fib : Integer -> Integer
-fib 0 = 1
-fib 1 = 1
-fib n = fib (n-1) + fib (n-2)
-
-fibNat : Nat -> Nat
-fibNat Zero = Succ Zero
-fibNat (Succ Zero) = Succ Zero
-fibNat (Succ (Succ n)) = plus Nat add_Nat (fibNat (Succ n)) (fibNat n)
\ No newline at end of file
diff --git a/transfer/examples/layout.tra b/transfer/examples/layout.tra
deleted file mode 100644
index 8c2d9aa3f..000000000
--- a/transfer/examples/layout.tra
+++ /dev/null
@@ -1,9 +0,0 @@
-x : Apa
-x = let x = y 
-     in case y of
-         f -> q
-         _ -> a
-
-f = apa 
-
-g = bepa
\ No newline at end of file
diff --git a/transfer/examples/list.tra b/transfer/examples/list.tra
deleted file mode 100644
index 253c29e02..000000000
--- a/transfer/examples/list.tra
+++ /dev/null
@@ -1,6 +0,0 @@
-import prelude
-
-l1 = append ? [1,2,3,5,6] [3]
-l2 = 2 :: l1
-
-main = rec { x = length ? l2; y = l2}
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)
-
diff --git a/transfer/examples/reflexive/Abstract.gf b/transfer/examples/reflexive/Abstract.gf
deleted file mode 100644
index 0426defdc..000000000
--- a/transfer/examples/reflexive/Abstract.gf
+++ /dev/null
@@ -1,15 +0,0 @@
-abstract Abstract = {
-
-cat 
-  S ; NP ; V2 ; Conj ;
-
-fun
-  PredV2 : V2 -> NP -> NP -> S ;
-  ReflV2 : V2 -> NP -> S ;
-  ConjNP : Conj -> NP -> NP -> NP ;
-
-  And, Or : Conj ;
-  John, Mary, Bill : NP ;
-  See, Whip : V2 ;
-
-}
diff --git a/transfer/examples/reflexive/English.gf b/transfer/examples/reflexive/English.gf
deleted file mode 100644
index 73fa00e91..000000000
--- a/transfer/examples/reflexive/English.gf
+++ /dev/null
@@ -1,54 +0,0 @@
-concrete English of Abstract = {
-
-lincat 
-  S = { s : Str } ;
-  V2 = {s : Num => Str} ;
-  Conj = {s : Str ; n : Num} ;
-  NP = {s : Str ; n : Num; g : Gender} ;
-
-lin
-  PredV2 v s o = ss (s.s ++ v.s ! s.n ++ o.s) ;
-  ReflV2 v s = ss (s.s ++ v.s ! s.n ++ self ! s.n ! s.g) ;
-  -- FIXME: what is the gender of "Mary or Bill"?
-  ConjNP c A B = {s = A.s ++ c.s ++ B.s ; n = c.n; g = A.g } ; 
-  
-  John = pn Masc "John" ;
-  Mary = pn Fem "Mary" ;
-  Bill = pn Masc "Bill" ;
-  See = regV2 "see" ;
-  Whip = regV2 "whip" ;
-
-  And = {s = "and" ; n = Pl } ;
-  Or = { s = "or"; n = Sg } ;
-
-param
-  Num = Sg | Pl ;
-  Gender = Neutr | Masc | Fem ;
-
-oper
-  regV2 : Str -> {s : Num => Str} = \run -> {
-    s = table {
-      Sg => run + "s" ;
-      Pl => run
-      }
-    } ;
-
-  self : Num => Gender => Str =
-    table {
-      Sg => table {
-	     Neutr => "itself";
-	     Masc  => "himself";
-	     Fem   => "herself"
-	};
-      Pl => \\g => "themselves"
-    };
-
-  pn : Gender -> Str -> {s : Str ; n : Num; g : Gender} = \gen -> \bob -> {
-    s = bob ;
-    n = Sg ;
-    g = gen
-    } ;
-
-  ss : Str -> {s : Str} = \s -> {s = s} ;
-
-}
diff --git a/transfer/examples/reflexive/reflexive.tra b/transfer/examples/reflexive/reflexive.tra
deleted file mode 100644
index 8d28f0db0..000000000
--- a/transfer/examples/reflexive/reflexive.tra
+++ /dev/null
@@ -1,40 +0,0 @@
-{-
-
-$ ../../transferc -i../../lib reflexive.tra
-
-$ gf English.gf reflexive.trc
-
-> p -tr "John sees John" | at -tr reflexivize_S | l
-PredV2 See John John
-ReflV2 See John
-John sees himself
-
-> p -tr "John and Bill see John and Bill" | at -tr reflexivize_S | l
-PredV2 See (ConjNP And John Bill) (ConjNP And John Bill)
-ReflV2 See (ConjNP And John Bill)
-John and Bill see themselves
-
-> p -tr "John sees Mary" | at -tr reflexivize_S | l
-PredV2 See John Mary
-PredV2 See John Mary
-John sees Mary
-
--}
-
-import tree
-
-reflexivize : (C : Cat) -> Tree C -> Tree C
-reflexivize _ (PredV2 v s o) | eq ? (eq_Tree ?) s o = ReflV2 v s
-reflexivize _ t = composOp ? ? compos_Tree ? reflexivize t
-
-reflexivize_S : Tree S -> Tree S
-reflexivize_S = reflexivize S
-
-{-
-With a type checker and hidden arguments we could write:
-
-reflexivize : {C : Cat} -> Tree C -> Tree C
-reflexivize (PredV2 v s o) | s == o = ReflV2 v s
-reflexivize t = composOp reflexivize t
-
--}
\ No newline at end of file
diff --git a/transfer/examples/reflexive/tree.tra b/transfer/examples/reflexive/tree.tra
deleted file mode 100644
index 7bef5e019..000000000
--- a/transfer/examples/reflexive/tree.tra
+++ /dev/null
@@ -1,21 +0,0 @@
-import prelude ;
-data Cat : Type where {
-  Conj : Cat ;
-  NP : Cat ;
-  S : Cat ;
-  V2 : Cat 
-} ;
-data Tree : Cat -> Type where {
-  And : Tree Conj ;
-  Bill : Tree NP ;
-  ConjNP : Tree Conj -> Tree NP -> Tree NP -> Tree NP ;
-  John : Tree NP ;
-  Mary : Tree NP ;
-  Or : Tree Conj ;
-  PredV2 : Tree V2 -> Tree NP -> Tree NP -> Tree S ;
-  ReflV2 : Tree V2 -> Tree NP -> Tree S ;
-  See : Tree V2 ;
-  Whip : Tree V2 
-} ;
-derive Eq Tree ;
-derive Compos Tree ;
diff --git a/transfer/examples/stoneage.tra b/transfer/examples/stoneage.tra
deleted file mode 100644
index e48c519e6..000000000
--- a/transfer/examples/stoneage.tra
+++ /dev/null
@@ -1,210 +0,0 @@
-import prelude
-
-data Cat : Type where {
-  CN : Cat ;
-  NP : Cat ;
-  S : Cat
-} ;
-data Tree : (_ : Cat)-> Type where {
-  A : (h_ : Tree CN)-> Tree NP ;
-  All : (h_ : Tree CN)-> Tree NP ;
-  Animal : Tree CN ;
-  Ashes : Tree CN ;
-  Back : Tree CN ;
-  Bad : (h_ : Tree CN)-> Tree CN ;
-  Bark : Tree CN ;
-  Belly : Tree CN ;
-  Big : (h_ : Tree CN)-> Tree CN ;
-  Bird : Tree CN ;
-  Bite : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
-  Black : (h_ : Tree CN)-> Tree CN ;
-  Blood : Tree CN ;
-  Blow : (h_ : Tree NP)-> Tree S ;
-  Bone : Tree CN ;
-  Breast : Tree CN ;
-  Breathe : (h_ : Tree NP)-> Tree S ;
-  Burn : (h_ : Tree NP)-> Tree S ;
-  Child : Tree CN ;
-  Cloud : Tree CN ;
-  Cold : (h_ : Tree CN)-> Tree CN ;
-  Come : (h_ : Tree NP)-> Tree S ;
-  Correct : (h_ : Tree CN)-> Tree CN ;
-  Count : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
-  Cut : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
-  Day : Tree CN ;
-  Die : (h_ : Tree NP)-> Tree S ;
-  Dig : (h_ : Tree NP)-> Tree S ;
-  Dirty : (h_ : Tree CN)-> Tree CN ;
-  Dog : Tree CN ;
-  Drink : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
-  Dry : (h_ : Tree CN)-> Tree CN ;
-  Dull : (h_ : Tree CN)-> Tree CN ;
-  Dust : Tree CN ;
-  Ear : Tree CN ;
-  Earth : Tree CN ;
-  Eat : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
-  Egg : Tree CN ;
-  Eye : Tree CN ;
-  Fall : (h_ : Tree NP)-> Tree S ;
-  Fat : Tree CN ;
-  Father : Tree CN ;
-  FatherOf : (h_ : Tree NP)-> Tree CN ;
-  Fear : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
-  Feather : Tree CN ;
-  Few : (h_ : Tree CN)-> Tree NP ;
-  Fight : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
-  Fingernail : Tree CN ;
-  Fire : Tree CN ;
-  Fish : Tree CN ;
-  Five : (h_ : Tree CN)-> Tree NP ;
-  Float : (h_ : Tree NP)-> Tree S ;
-  Flow : (h_ : Tree NP)-> Tree S ;
-  Flower : Tree CN ;
-  Fly : (h_ : Tree NP)-> Tree S ;
-  Fog : Tree CN ;
-  Foot : Tree CN ;
-  Forest : Tree CN ;
-  Four : (h_ : Tree CN)-> Tree NP ;
-  Freeze : (h_ : Tree NP)-> Tree S ;
-  Fruit : Tree CN ;
-  Full : (h_ : Tree CN)-> Tree CN ;
-  Give : (h_ : Tree NP)-> (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
-  Good : (h_ : Tree CN)-> Tree CN ;
-  Grass : Tree CN ;
-  Green : (h_ : Tree CN)-> Tree CN ;
-  Guts : Tree CN ;
-  Hair : Tree CN ;
-  Hand : Tree CN ;
-  He : Tree NP ;
-  Head : Tree CN ;
-  Hear : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
-  Heart : Tree CN ;
-  Heavy : (h_ : Tree CN)-> Tree CN ;
-  Hit : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
-  Hold : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
-  Horn : Tree CN ;
-  Hunt : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
-  Husband : Tree CN ;
-  I : Tree NP ;
-  Ice : Tree CN ;
-  Kill : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
-  Knee : Tree CN ;
-  Know : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
-  Lake : Tree CN ;
-  Laugh : (h_ : Tree NP)-> Tree S ;
-  Leaf : Tree CN ;
-  Left : (h_ : Tree CN)-> Tree CN ;
-  Leg : Tree CN ;
-  Lie : (h_ : Tree NP)-> Tree S ;
-  Live : (h_ : Tree NP)-> Tree S ;
-  Liver : Tree CN ;
-  Long : (h_ : Tree CN)-> Tree CN ;
-  Louse : Tree CN ;
-  Man : Tree CN ;
-  Many : (h_ : Tree CN)-> Tree NP ;
-  Meat : Tree CN ;
-  Moon : Tree CN ;
-  Mother : Tree CN ;
-  MotherOf : (h_ : Tree NP)-> Tree CN ;
-  Mountain : Tree CN ;
-  Mouth : Tree CN ;
-  Name : Tree CN ;
-  Narrow : (h_ : Tree CN)-> Tree CN ;
-  Near : (h_ : Tree CN)-> Tree CN ;
-  Neck : Tree CN ;
-  New : (h_ : Tree CN)-> Tree CN ;
-  Night : Tree CN ;
-  Nose : Tree CN ;
-  Old : (h_ : Tree CN)-> Tree CN ;
-  One : (h_ : Tree CN)-> Tree NP ;
-  Other : (h_ : Tree CN)-> Tree NP ;
-  Person : Tree CN ;
-  Play : (h_ : Tree NP)-> Tree S ;
-  Pull : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
-  Push : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
-  Rain : Tree CN ;
-  Red : (h_ : Tree CN)-> Tree CN ;
-  Right : (h_ : Tree CN)-> Tree CN ;
-  River : Tree CN ;
-  Road : Tree CN ;
-  Root : Tree CN ;
-  Rope : Tree CN ;
-  Rotten : (h_ : Tree CN)-> Tree CN ;
-  Round : (h_ : Tree CN)-> Tree CN ;
-  Rub : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
-  Salt : Tree CN ;
-  Sand : Tree CN ;
-  Scratch : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
-  Sea : Tree CN ;
-  See : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
-  Seed : Tree CN ;
-  Sew : (h_ : Tree NP)-> Tree S ;
-  Sharp : (h_ : Tree CN)-> Tree CN ;
-  Short : (h_ : Tree CN)-> Tree CN ;
-  Sing : (h_ : Tree NP)-> Tree S ;
-  Sit : (h_ : Tree NP)-> Tree S ;
-  Skin : Tree CN ;
-  Sky : Tree CN ;
-  Sleep : (h_ : Tree NP)-> Tree S ;
-  Small : (h_ : Tree CN)-> Tree CN ;
-  Smell : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
-  Smoke : Tree CN ;
-  Smooth : (h_ : Tree CN)-> Tree CN ;
-  Snake : Tree CN ;
-  Snow : Tree CN ;
-  Some_Many : (h_ : Tree CN)-> Tree NP ;
-  Some_One : (h_ : Tree CN)-> Tree NP ;
-  Spit : (h_ : Tree NP)-> Tree S ;
-  Split : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
-  Squeeze : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
-  Stab : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
-  Stand : (h_ : Tree NP)-> Tree S ;
-  Star : Tree CN ;
-  Stick : Tree CN ;
-  Stone : Tree CN ;
-  Straight : (h_ : Tree CN)-> Tree CN ;
-  Suck : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
-  Sun : Tree CN ;
-  Swell : (h_ : Tree NP)-> Tree S ;
-  Swim : (h_ : Tree NP)-> Tree S ;
-  Tail : Tree CN ;
-  That : (h_ : Tree CN)-> Tree NP ;
-  The_Many : (h_ : Tree CN)-> Tree NP ;
-  The_One : (h_ : Tree CN)-> Tree NP ;
-  They : Tree NP ;
-  Thick : (h_ : Tree CN)-> Tree CN ;
-  Thin : (h_ : Tree CN)-> Tree CN ;
-  Think : (h_ : Tree NP)-> Tree S ;
-  This : (h_ : Tree CN)-> Tree NP ;
-  Three : (h_ : Tree CN)-> Tree NP ;
-  Throw : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
-  Tie : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
-  Tongue : Tree CN ;
-  Tooth : Tree CN ;
-  Tree : Tree CN ;
-  Turn : (h_ : Tree NP)-> Tree S ;
-  Two : (h_ : Tree CN)-> Tree NP ;
-  Vomit : (h_ : Tree NP)-> Tree S ;
-  Walk : (h_ : Tree NP)-> Tree S ;
-  Warm : (h_ : Tree CN)-> Tree CN ;
-  Wash : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
-  Water : Tree CN ;
-  We : Tree NP ;
-  Wet : (h_ : Tree CN)-> Tree CN ;
-  White : (h_ : Tree CN)-> Tree CN ;
-  Wide : (h_ : Tree CN)-> Tree CN ;
-  Wife : Tree CN ;
-  Wind : Tree CN ;
-  Wing : Tree CN ;
-  Wipe : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
-  Woman : Tree CN ;
-  Worm : Tree CN ;
-  Year : Tree CN ;
-  Yellow : (h_ : Tree CN)-> Tree CN ;
-  You_Many : Tree NP ;
-  You_One : Tree NP
-}
-
-derive Compos Tree
-
-derive Eq Tree
\ No newline at end of file
diff --git a/transfer/examples/test.tra b/transfer/examples/test.tra
deleted file mode 100644
index bfd303ee5..000000000
--- a/transfer/examples/test.tra
+++ /dev/null
@@ -1,4 +0,0 @@
-import nat
-import fib
-
-main = (\x -> (\x -> \x -> x) 1 x) 5
diff --git a/transfer/examples/tricky-type-checking.tra b/transfer/examples/tricky-type-checking.tra
deleted file mode 100644
index ad69c33db..000000000
--- a/transfer/examples/tricky-type-checking.tra
+++ /dev/null
@@ -1,37 +0,0 @@
-
---
--- Pattern matching and inductive families.
---
-
-data Tree : Type -> Type where
-  EAdd : Tree Integer -> Tree Integer -> Tree Integer
-  EInt : Integer -> Tree Integer
-  EFoo : (A:Type) -> A -> Tree A
-
-eval : (B : Type) -> Tree B -> Tree B
-eval _ t = case t of
-		EAdd x y -> EInt (x+y)
-		EInt i -> EInt i
-		EFoo T x -> EFoo T x
-
-strip : (B : Type) -> Tree B -> B
-strip _ t = case t of
-		EAdd x y -> x+y
-		EInt i -> i
-		EFoo _ x -> x
-
---
--- Subtyping
---
-
-getX : { x : Integer } -> Integer
-getX r = r.x
-
-getY : { y : Integer } -> Integer
-getY r = r.y
-
-proj2 : (A:Type) -> (B:Type) -> (C:Type) -> (A -> B) -> (A -> C) -> A -> (B,C)
-proj2 _ _ _ f g x = (f x, g x)
-
-getXY : { x : Integer, y : Integer } -> (Integer,Integer)
-getXY r = proj2 ? ? ? getX getY r
diff --git a/transfer/examples/widesnake.tra b/transfer/examples/widesnake.tra
deleted file mode 100644
index f68ed9013..000000000
--- a/transfer/examples/widesnake.tra
+++ /dev/null
@@ -1,21 +0,0 @@
-import bool
-import stoneage
-
-monoid_Bool : sig { zero : Bool; plus : Bool -> Bool -> Bool }
-monoid_Bool = rec
-	        zero = False
-	        plus = \x -> \y -> x && y
-
-isSnake : (A : Tree) -> Tree A -> Bool
-isSnake _ x = case x of
-		Snake -> True
-		_ -> composFold ? ? compos_Tree Bool monoid_Bool ? isSnake x
-
-wideSnake : (A : Cat) -> Tree A -> Tree A
-wideSnake _ x = case x of
-		    Wide y -> let y' = wideSnake ? y
-                               in if isSnake CN y' then Thick y' else Wide y'
-		    _ -> composOp ? ? compos_Tree ? wideSnake x
-		
-wideSnakeNP : Tree NP -> Tree NP
-wideSnakeNP = wideSnake NP