summaryrefslogtreecommitdiff
path: root/transfer/examples/list.tr
diff options
context:
space:
mode:
authorbringert <bringert@cs.chalmers.se>2005-11-28 21:45:22 +0000
committerbringert <bringert@cs.chalmers.se>2005-11-28 21:45:22 +0000
commit02c23401a7a3e54d48084fc2796a485de36383f1 (patch)
tree03574e9f1c862f2b5685741c6c9d8ee8029aea21 /transfer/examples/list.tr
parent5a82068ddc0e75ee2f2280ffb5da9cda3e53bac3 (diff)
Changed all example programs to use layout syntax.
Diffstat (limited to 'transfer/examples/list.tr')
-rw-r--r--transfer/examples/list.tr24
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)