aboutsummaryrefslogtreecommitdiffhomepage
path: root/demo/more/versioned.urs
diff options
context:
space:
mode:
Diffstat (limited to 'demo/more/versioned.urs')
-rw-r--r--demo/more/versioned.urs19
1 files changed, 19 insertions, 0 deletions
diff --git a/demo/more/versioned.urs b/demo/more/versioned.urs
new file mode 100644
index 00000000..eb0a485e
--- /dev/null
+++ b/demo/more/versioned.urs
@@ -0,0 +1,19 @@
+functor Make(M : sig
+ con key :: {Type}
+ con data :: {Type}
+ constraint key ~ data
+ constraint [When] ~ (key ++ data)
+
+ val key : $(map sql_injectable key)
+ val data : $(map (fn t => {Inj : sql_injectable_prim t,
+ Eq : eq t}) data)
+
+ val keyFolder : folder key
+ val dataFolder : folder data
+ end) : sig
+ val insert : $(M.key ++ M.data) -> transaction unit
+ val update : $(M.key ++ M.data) -> transaction unit
+
+ val keys : transaction (list $M.key)
+ val current : $M.key -> transaction (option $M.data)
+end