From dbe8e61acc616b8f5ac07e8df89eb98a7997c29d Mon Sep 17 00:00:00 2001 From: bringert Date: Fri, 25 Nov 2005 16:36:19 +0000 Subject: Move transfer into the GF repo. --- transfer/examples/list.tr | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) create mode 100644 transfer/examples/list.tr (limited to 'transfer/examples/list.tr') 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) ; -- cgit v1.2.3