Ur/Web: tests/specialize.ur annotate

Unpoly non-recursive function

author	Adam Chlipala <adamc@hcoop.net>
date	Thu, 11 Sep 2008 09:36:47 -0400
parents
children	04ebfe929a98

rev	line source
adamc@315	1 datatype list a = Nil \| Cons of a * list a
adamc@315	2
adamc@315	3 fun isNil (t ::: Type) (ls : list t) : bool =
adamc@315	4 case ls of
adamc@315	5 Nil => True
adamc@315	6 \| Cons _ => False
adamc@315	7
adamc@315	8 (*fun append (t ::: Type) (ls1 : list t) (ls2 : list t) : list t =
adamc@315	9 case ls1 of
adamc@315	10 Nil => ls2
adamc@315	11 \| Cons (x, ls1') => Cons (x, append ls1' ls2)
adamc@315	12
adamc@315	13 fun delist (ls : list string) : xml body [] [] =
adamc@315	14 case ls of
adamc@315	15 Nil => <body>Nil</body>
adamc@315	16 \| Cons (h, t) => <body>{cdata h} :: {delist t}</body>*)
adamc@315	17
adamc@315	18 val ls = Cons ("X", Cons ("Y", Cons ("Z", Nil)))
adamc@315	19
adamc@315	20 fun main () : transaction page = return <html><body>
adamc@315	21 {if isNil ls then <body>It's Nil.</body> else <body>It's not Nil.</body>}
adamc@315	22 </body></html>
adamc@315	23
adamc@315	24
adamc@315	25 (* <p>{delist ls}</p>*)
adamc@315	26

Mercurial > urweb