diff options
| author | bringert <bringert@cs.chalmers.se> | 2005-11-28 21:45:22 +0000 |
|---|---|---|
| committer | bringert <bringert@cs.chalmers.se> | 2005-11-28 21:45:22 +0000 |
| commit | 02c23401a7a3e54d48084fc2796a485de36383f1 (patch) | |
| tree | 03574e9f1c862f2b5685741c6c9d8ee8029aea21 /transfer/examples/list.tr | |
| parent | 5a82068ddc0e75ee2f2280ffb5da9cda3e53bac3 (diff) | |
Changed all example programs to use layout syntax.
Diffstat (limited to 'transfer/examples/list.tr')
| -rw-r--r-- | transfer/examples/list.tr | 24 |
1 files changed, 12 insertions, 12 deletions
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) |
