Ur/Web: demo/treeFun.urs annotate

Coq formalization uses TDisjoint

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

rev	line source
adamc@469	1 functor Make(M : sig
adamc@469	2 type key
adamc@469	3 con id :: Name
adamc@469	4 con parent :: Name
adamc@469	5 con cols :: {Type}
adamc@469	6 constraint [id] ~ [parent]
adamc@469	7 constraint [id, parent] ~ cols
adamc@469	8
adamc@469	9 val key_inj : sql_injectable key
adamc@469	10 val option_key_inj : sql_injectable (option key)
adamc@469	11
adamc@469	12 table tab : [id = key, parent = option key] ++ cols
adamc@469	13 end) : sig
adamc@469	14
adamc@469	15 con id = M.id
adamc@469	16 con parent = M.parent
adamc@469	17
adamc@469	18 val tree : ($([id = M.key, parent = option M.key] ++ M.cols) -> xbody)
adamc@469	19 -> option M.key
adamc@469	20 -> transaction xbody
adamc@469	21
adamc@469	22 end

Mercurial > urweb