comparison lib/top.ur @ 559:5d494183ca89

Add SQL arithmetic operators
author Adam Chlipala <adamc@hcoop.net>
date Tue, 09 Dec 2008 14:41:19 -0500
parents 20fab0e96217
children 803b2f3bb86b
comparison
equal deleted inserted replaced
558:390cba747188 559:5d494183ca89
236 (t ::: Type) (inj : sql_injectable (option t)) 236 (t ::: Type) (inj : sql_injectable (option t))
237 (e1 : sql_exp tables agg exps (option t)) 237 (e1 : sql_exp tables agg exps (option t))
238 (e2 : option t) = 238 (e2 : option t) =
239 case e2 of 239 case e2 of
240 None => (SQL {e1} IS NULL) 240 None => (SQL {e1} IS NULL)
241 | Some _ => sql_comparison sql_eq e1 (@sql_inject inj e2) 241 | Some _ => sql_binary sql_eq e1 (@sql_inject inj e2)