diff lib/ur/top.urs @ 1074:d89f98f0b4bb

Fixing a bug in DInitializer elaboration
author Adam Chlipala <adamc@hcoop.net>
date Sun, 13 Dec 2009 14:34:18 -0500
parents 9001966ae1c8
children dcf98ae3c48d
line wrap: on
line diff
--- a/lib/ur/top.urs	Sun Dec 13 14:20:41 2009 -0500
+++ b/lib/ur/top.urs	Sun Dec 13 14:34:18 2009 -0500
@@ -173,6 +173,9 @@
     sql_query (mapU [] tabs) [nm = t]
     -> transaction t
 
+val nonempty : fs ::: {Type} -> us ::: {{Unit}} -> sql_table fs us
+               -> transaction bool
+
 val eqNullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
                  -> t ::: Type -> sql_injectable (option t)
                  -> sql_exp tables agg exps (option t)