Simple transfer tutorial touch-up.

1 files changed, 24 insertions, 25 deletions

diff --git a/transfer/examples/aggregation/aggregate.tr b/transfer/examples/aggregation/aggregate.tr
index 7cdfaddca..b71ccfef2 100644
--- a/transfer/examples/aggregation/aggregate.tr
+++ b/transfer/examples/aggregation/aggregate.tr
@@ -1,13 +1,31 @@
 import prelude
 import tree
 
-derive Eq Tree
-derive Compos 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:
 {-
+-- When the Transfer compiler gets meta variable inference,
+-- we can write this:
 aggreg : (A : Type) -> Tree A -> Tree A
 aggreg _ t = 
   case t of
@@ -21,8 +39,9 @@ aggreg _ t =
       _ -> composOp ? ? ? ? aggreg t
 -}
 
--- Adding hidden arguments, we could write something like:
+
 {-
+-- If we added idden arguments, we could write something like this:
 aggreg : (A : Type) => Tree A -> Tree A
 aggreg t = 
   case t of
@@ -35,23 +54,3 @@ aggreg t =
 		(s1',s2') -> ConjS c s1' s2'
       _ -> composOp aggreg t
 -}
-
-
--- 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
-
-
--- aggreg specialized for Tree S
-aggregS : Tree S -> Tree S
-aggregS = aggreg S