comparison tests/specialize.ur @ 315:e21d0dddda09

Unpoly non-recursive function
author Adam Chlipala <adamc@hcoop.net>
date Thu, 11 Sep 2008 09:36:47 -0400
parents
children 04ebfe929a98
comparison
equal deleted inserted replaced
314:a07f476d9b61 315:e21d0dddda09
1 datatype list a = Nil | Cons of a * list a
2
3 fun isNil (t ::: Type) (ls : list t) : bool =
4 case ls of
5 Nil => True
6 | Cons _ => False
7
8 (*fun append (t ::: Type) (ls1 : list t) (ls2 : list t) : list t =
9 case ls1 of
10 Nil => ls2
11 | Cons (x, ls1') => Cons (x, append ls1' ls2)
12
13 fun delist (ls : list string) : xml body [] [] =
14 case ls of
15 Nil => <body>Nil</body>
16 | Cons (h, t) => <body>{cdata h} :: {delist t}</body>*)
17
18 val ls = Cons ("X", Cons ("Y", Cons ("Z", Nil)))
19
20 fun main () : transaction page = return <html><body>
21 {if isNil ls then <body>It's Nil.</body> else <body>It's not Nil.</body>}
22 </body></html>
23
24
25 (* <p>{delist ls}</p>*)
26