summaryrefslogtreecommitdiff
path: root/tests/list.ur
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-04-30 15:10:13 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-04-30 15:10:13 -0400
commitd4646bbb7f107e3c773bec5e18fd44f435ac40ca (patch)
tree5ce0fa4602a456daa6d78bcf1f1ea68fb73174dc /tests/list.ur
parent72414e8531db237906a847fe1a7adaed4b000978 (diff)
List notations
Diffstat (limited to 'tests/list.ur')
-rw-r--r--tests/list.ur16
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>