Mercurial > urweb
comparison lib/ur/basis.urs @ 1207:ae3036773768
Introduced the known() predicate
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 06 Apr 2010 09:51:36 -0400 |
parents | c316ca3c9ec6 |
children | 648e6b087dfb |
comparison
equal
deleted
inserted
replaced
1206:772760df4c4c | 1207:ae3036773768 |
---|---|
496 val sql_ufunc : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} | 496 val sql_ufunc : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} |
497 -> dom ::: Type -> ran ::: Type | 497 -> dom ::: Type -> ran ::: Type |
498 -> sql_ufunc dom ran -> sql_exp tables agg exps dom | 498 -> sql_ufunc dom ran -> sql_exp tables agg exps dom |
499 -> sql_exp tables agg exps ran | 499 -> sql_exp tables agg exps ran |
500 val sql_octet_length : sql_ufunc blob int | 500 val sql_octet_length : sql_ufunc blob int |
501 val sql_known : t ::: Type -> sql_ufunc t bool | |
501 | 502 |
502 | 503 |
503 val sql_nullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type | 504 val sql_nullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type |
504 -> sql_injectable_prim t | 505 -> sql_injectable_prim t |
505 -> sql_exp tables agg exps t | 506 -> sql_exp tables agg exps t |