From cba2fcb9b118cedb603b171ac7d7581c5adb844c Mon Sep 17 00:00:00 2001 From: bringert Date: Wed, 30 Nov 2005 16:00:06 +0000 Subject: Moved transfer libraries to transfer/lib --- transfer/lib/list.tr | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) create mode 100644 transfer/lib/list.tr (limited to 'transfer/lib/list.tr') diff --git a/transfer/lib/list.tr b/transfer/lib/list.tr new file mode 100644 index 000000000..079208167 --- /dev/null +++ b/transfer/lib/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