SELECT DISTINCT; eta expansion during Cjrization

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