Changes between Version 6 and Version 7 of TypeFunctionsSynTC

Timestamp:

12/07/06 11:58:36 (6 years ago)

Author:

chak

Comment:

Fixed syntax in introductory example

TypeFunctionsSynTC

@@ -24 +24 @@
 data Succ n
 data List a n where
-  Nil :: List a Zero
+  Nil  :: List a Zero
   Cons :: a -> List a m -> List a (Succ m)
 
-type add :: * -> * -> *
-     add Zero x = x
-     add (Succ x) y = Succ (add x y)
-
-append :: List a l -> List a m -> List a (add l m)
+type family Add :: * -> * -> *
+type instance Add Zero     y = y
+type instance Add (Succ x) y = Succ (Add x y)
+
+append :: List a l -> List a m -> List a (Add l m)
 append Nil xs = xs
 append (Cons x xs) ys = Cons x (append xs ys)