1 files changed, 17 insertions, 0 deletions
diff --git a/transfer/examples/list.tr b/transfer/examples/list.tr
new file mode 100644
index 000000000..f31278f54
--- /dev/null
+++ b/transfer/examples/list.tr
@@ -0,0 +1,17 @@
+import nat ;
+
+data List : (_:Type) -> Type where 
+	{ Nil : (A:Type) -> List A ;
+          Cons : (A:Type) -> A -> List A -> List A ; } ;
+
+size : (A:Type) -> List A -> Nat ;
+size _ (Nil _) = Zero ;
+size A (Cons _ x xs) = Succ (size A xs) ;
+
+map : (A:Type) -> (B:Type) -> (A -> B) -> List A -> List B ;
+map _ B _ (Nil _) = Nil B ;
+map A B f (Cons _ x xs) = Cons B (f x) (map A B f xs) ;
+
+append : (A:Type) -> (xs:List A) -> List A -> List A ;
+append _ (Nil _) ys = ys ;
+append A (Cons _ x xs) ys = Cons A x (append A xs ys) ;