Ur/Web: tests/dlist2.ur annotate

Coq formalization uses TDisjoint

author	Adam Chlipala <adamc@hcoop.net>
date	Tue, 24 Feb 2009 16:08:14 -0500
parents	1a9171e31fd1
children

rev	line source
adamc@605	1 datatype dlist = Nil \| Cons of string * source dlist
adamc@605	2
adamc@605	3 fun delist dl =
adamc@605	4 case dl of
adamc@605	5 Nil => <xml>[]</xml>
adamc@605	6 \| Cons (x, s) => <xml>{[x]} <ctextbox/> :: {delistSource s}</xml>
adamc@605	7
adamc@605	8 and delistSource s = <xml><dyn signal={dl <- signal s; return (delist dl)}/></xml>
adamc@605	9
adamc@605	10 fun main () : transaction page =
adamc@605	11 tail0 <- source Nil;
adamc@605	12 tail <- source tail0;
adamc@605	13 tb <- source "";
adamc@605	14 return <xml><body>
adamc@605	15 {delist (Cons ("ROOT", tail0))}
adamc@605	16 <br/>
adamc@605	17 <ctextbox source={tb}/>
adamc@605	18 <button value="Add" onclick={hd <- get tb;
adamc@605	19 tl <- source Nil;
adamc@605	20 old <- get tail;
adamc@605	21
adamc@605	22 set old (Cons (hd, tl));
adamc@605	23 set tail tl}/>
adamc@605	24 <button value="Reset" onclick={set tail0 Nil; set tail tail0}/>
adamc@605	25 </body></xml>

Mercurial > urweb