diff lib/ur/basis.urs @ 1427:541673c3161d

sql_arith_option; 'ALL' for relational operators
author Adam Chlipala <adam@chlipala.net>
date Fri, 25 Feb 2011 11:27:16 -0500
parents 3dab4696d116
children aae3e3b6a408
line wrap: on
line diff
--- a/lib/ur/basis.urs	Tue Feb 22 09:39:02 2011 -0500
+++ b/lib/ur/basis.urs	Fri Feb 25 11:27:16 2011 -0500
@@ -384,6 +384,7 @@
                 -> selectedFields ::: {{Type}}
                 -> selectedExps ::: {Type}
                 -> sql_relop
+                -> bool (* ALL *)
                 -> sql_query1 free afree tables1 selectedFields selectedExps
                 -> sql_query1 free afree tables2 selectedFields selectedExps
                 -> sql_query1 free afree [] selectedFields selectedExps
@@ -448,8 +449,9 @@
                   -> sql_exp tables agg exps bool
 
 class sql_arith
-val sql_int_arith : sql_arith int
-val sql_float_arith : sql_arith float
+val sql_arith_int : sql_arith int
+val sql_arith_float : sql_arith float
+val sql_arith_option : t ::: Type -> sql_arith t -> sql_arith (option t)
 
 con sql_unary :: Type -> Type -> Type
 val sql_not : sql_unary bool bool