Ur/Web: tests/unurlify.ur annotate

Hooks for measuring how much interesting proving is going on in elaboration

author	Adam Chlipala <adamc@hcoop.net>
date	Tue, 17 Nov 2009 12:44:14 -0500
parents	ebf27030ae3b
children

rev	line source
adamc@398	1 datatype list t = Nil \| Cons of t * list t
adamc@398	2
adamc@398	3 fun handler (ls : list bool) = return <xml/>
adamc@398	4
adamc@402	5 datatype wlist = WNil \| Empty \| WCons of bool * wlist
adamc@402	6
adamc@402	7 fun whandler' (ls : wlist) =
adamc@402	8 case ls of
adamc@402	9 WNil => <xml>Nil</xml>
adamc@402	10 \| Empty => <xml>Empty</xml>
adamc@402	11 \| WCons (x, ls') => <xml>{[x]} :: {whandler' ls'}</xml>
adamc@402	12
adamc@402	13 fun whandler ls = return (whandler' ls)
adamc@402	14
adamc@398	15 fun main () : transaction page = return <xml><body>
adamc@402	16 <a link={handler Nil}>!</a><br/>
adamc@402	17 <a link={whandler WNil}>Nil</a><br/>
adamc@402	18 <a link={whandler Empty}>Empty</a><br/>
adamc@402	19 <a link={whandler (WCons (True, WCons (False, Empty)))}>True :: False :: Empty</a><br/>
adamc@398	20 </body></xml>

Mercurial > urweb