Ur/Web: tests/option.ur annotate

Some small changes while failing to write [restrict]

author	Adam Chlipala <adamc@hcoop.net>
date	Sat, 08 Nov 2008 13:15:00 -0500
parents	77a28e7430bf
children

rev	line source
adamc@198	1 datatype option a = None \| Some of a
adamc@198	2
adamc@198	3 val none_Hi : option string = None
adamc@198	4 val some_Hi = Some "Hi"
adamc@198	5 val none_some_Hi : option (option string) = None
adamc@198	6 val some_some_Hi = Some some_Hi
adamc@198	7
adamc@198	8 val show = fn x => case x of None => "None" \| Some x => x
adamc@198	9
adamc@198	10 val show2 = fn x => case x of None => "None'" \| Some x => show x
adamc@198	11
adamc@284	12 val page = fn x => return <html><body>
adamc@198	13 {cdata (show x)}
adamc@198	14 </body></html>
adamc@198	15
adamc@284	16 val page2 = fn x => return <html><body>
adamc@198	17 {cdata (show2 x)}
adamc@198	18 </body></html>
adamc@198	19
adamc@284	20 val main : unit -> transaction page = fn () => return <html><body>
adamc@198	21 <li><a link={page none_Hi}>None1</a></li>
adamc@198	22 <li><a link={page some_Hi}>Some1</a></li>
adamc@198	23 <li><a link={page2 none_some_Hi}>None2</a></li>
adamc@198	24 <li><a link={page2 some_some_Hi}>Some2</a></li>
adamc@198	25 </body></html>

Mercurial > urweb