From 02c23401a7a3e54d48084fc2796a485de36383f1 Mon Sep 17 00:00:00 2001 From: bringert Date: Mon, 28 Nov 2005 21:45:22 +0000 Subject: Changed all example programs to use layout syntax. --- transfer/examples/list.tr | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) (limited to 'transfer/examples/list.tr') diff --git a/transfer/examples/list.tr b/transfer/examples/list.tr index f31278f54..079208167 100644 --- a/transfer/examples/list.tr +++ b/transfer/examples/list.tr @@ -1,17 +1,17 @@ -import nat ; +import nat data List : (_:Type) -> Type where - { Nil : (A:Type) -> List A ; - Cons : (A:Type) -> A -> List A -> List A ; } ; + 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) ; +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) ; +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) ; +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