Mercurial > urweb
view demo/more/dnat.ur @ 1034:a779402841f6
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 | e47303e5d73d |
children |
line wrap: on
line source
datatype t' = O | S of source t' type t = source t' val zero = source O fun inc n = v <- get n; case v of O => n' <- source O; set n (S n') | S n => inc n fun dec n = let fun dec' last n = v <- get n; case v of O => (case last of None => return () | Some n' => set n' O) | S n' => dec' (Some n) n' in dec' None n end fun render [ctx] [inp] [[Body] ~ ctx] (xml : xml ([Body] ++ ctx) inp []) n = let fun render n = n <- signal n; return (render' n) and render' n = case n of O => <xml/> | S n => <xml> {xml} <dyn signal={render n}/> </xml> in <xml><dyn signal={render n}/></xml> end