Ur/Web: tests/datatypeP.ur annotate

Instantiate any Unit unification variables that remain after elaboration

author	Adam Chlipala <adam@chlipala.net>
date	Thu, 02 Dec 2010 14:11:18 -0500
parents	71bafe66dbe1
children

rev	line source
adamc@191	1 datatype option a = None \| Some of a
adamc@191	2
adamc@191	3 val none : option int = None
adamc@191	4 val some_1 : option int = Some 1
adamc@191	5
adamc@191	6 val f = fn t ::: Type => fn x : option t =>
adamc@191	7 case x of None => None \| Some x => Some (Some x)
adamc@191	8
adamc@191	9 val none_again = f none
adamc@191	10 val some_1_again = f some_1
adamc@193	11
adamc@193	12 val show = fn t ::: Type => fn x : option t => case x of None => "None" \| Some _ => "Some"
adamc@193	13
adamc@193	14 val page = fn x => <html><body>
adamc@193	15 {cdata (show x)}
adamc@193	16 </body></html>
adamc@193	17
adamc@193	18 val main : unit -> page = fn () => <html><body>
adamc@193	19 <li><a link={page none_again}>None</a></li>
adamc@193	20 <li><a link={page some_1_again}>Some 1</a></li>
adamc@193	21 </body></html>

Mercurial > urweb