summaryrefslogtreecommitdiff
path: root/demo/more/dnat.urs
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-10-25 11:03:42 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-10-25 11:03:42 -0400
commit5e9435290876dcdfd3c66fb652257f4c3ed50697 (patch)
treee33effa1b155c3f40ceb8e3b1a80b937ae126547 /demo/more/dnat.urs
parente2ffafb9cfaf0bb921bc9bca491214cb464a38d7 (diff)
Factor Dnat into separate module
Diffstat (limited to 'demo/more/dnat.urs')
-rw-r--r--demo/more/dnat.urs8
1 files changed, 8 insertions, 0 deletions
diff --git a/demo/more/dnat.urs b/demo/more/dnat.urs
new file mode 100644
index 00000000..2dd7e938
--- /dev/null
+++ b/demo/more/dnat.urs
@@ -0,0 +1,8 @@
+type t
+
+val zero : transaction t
+val inc : t -> transaction unit
+val dec : t -> transaction unit
+
+val render : ctx ::: {Unit} -> inp ::: {Type} -> [[Body] ~ ctx] =>
+ xml ([Body] ++ ctx) inp [] -> t -> xml ([Body] ++ ctx) inp []