Mercurial > urweb
comparison tests/list.ur @ 762:9021d44ba6b2
List notations
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Thu, 30 Apr 2009 15:10:13 -0400 |
parents | 8323c1beef2e |
children |
comparison
equal
deleted
inserted
replaced
761:16b34dc2e29c | 762:9021d44ba6b2 |
---|---|
1 fun isNil (t ::: Type) (ls : list t) = | 1 fun isNil (t ::: Type) (ls : list t) = |
2 case ls of | 2 case ls of |
3 Nil => True | 3 [] => True |
4 | _ => False | 4 | _ => False |
5 | 5 |
6 fun delist (ls : list string) : xbody = | 6 fun delist (ls : list string) : xbody = |
7 case ls of | 7 case ls of |
8 Nil => <xml>Nil</xml> | 8 [] => <xml>Nil</xml> |
9 | Cons (h, t) => <xml>{[h]} :: {delist t}</xml> | 9 | h :: t => <xml>{[h]} :: {delist t}</xml> |
10 | 10 |
11 fun callback ls = return <xml><body> | 11 fun callback ls = return <xml><body> |
12 {delist ls} | 12 {delist ls} |
13 </body></xml> | 13 </body></xml> |
14 | 14 |
15 fun main () = return <xml><body> | 15 fun main () = return <xml><body> |
16 {[isNil (Nil : list bool)]}, | 16 {[isNil ([] : list bool)]}, |
17 {[isNil (Cons (1, Nil))]}, | 17 {[isNil (1 :: [])]}, |
18 {[isNil (Cons ("A", Cons ("B", Nil)))]} | 18 {[isNil ("A" :: "B" :: [])]} |
19 | 19 |
20 <p>{delist (Cons ("X", Cons ("Y", Cons ("Z", Nil))))}</p> | 20 <p>{delist ("X" :: "Y" :: "Z" :: [])}</p> |
21 <a link={callback (Cons ("A", Cons ("B", Nil)))}>Go!</a> | 21 <a link={callback ("A" :: "B" :: [])}>Go!</a> |
22 </body></xml> | 22 </body></xml> |