diff options
author | Adam Chlipala <adamc@hcoop.net> | 2009-04-30 15:10:13 -0400 |
---|---|---|
committer | Adam Chlipala <adamc@hcoop.net> | 2009-04-30 15:10:13 -0400 |
commit | 9977c20208ec6afcc1f9d97f145fa93d948bfa07 (patch) | |
tree | 5ce0fa4602a456daa6d78bcf1f1ea68fb73174dc /tests/list.ur | |
parent | 5b81f4d3c43a84e84355cbbc84aa6c8e9f3f5044 (diff) |
List notations
Diffstat (limited to 'tests/list.ur')
-rw-r--r-- | tests/list.ur | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/tests/list.ur b/tests/list.ur index 480bdd3e..472b9ea1 100644 --- a/tests/list.ur +++ b/tests/list.ur @@ -1,22 +1,22 @@ fun isNil (t ::: Type) (ls : list t) = case ls of - Nil => True + [] => True | _ => False fun delist (ls : list string) : xbody = case ls of - Nil => <xml>Nil</xml> - | Cons (h, t) => <xml>{[h]} :: {delist t}</xml> + [] => <xml>Nil</xml> + | h :: t => <xml>{[h]} :: {delist t}</xml> fun callback ls = return <xml><body> {delist ls} </body></xml> fun main () = return <xml><body> - {[isNil (Nil : list bool)]}, - {[isNil (Cons (1, Nil))]}, - {[isNil (Cons ("A", Cons ("B", Nil)))]} + {[isNil ([] : list bool)]}, + {[isNil (1 :: [])]}, + {[isNil ("A" :: "B" :: [])]} - <p>{delist (Cons ("X", Cons ("Y", Cons ("Z", Nil))))}</p> - <a link={callback (Cons ("A", Cons ("B", Nil)))}>Go!</a> + <p>{delist ("X" :: "Y" :: "Z" :: [])}</p> + <a link={callback ("A" :: "B" :: [])}>Go!</a> </body></xml> |