diff demo/more/meta.urs @ 1030:6bcc1020d5cd

Start of Decision
author Adam Chlipala <adamc@hcoop.net>
date Mon, 02 Nov 2009 15:48:06 -0500
parents 16f7cb0891b6
children
line wrap: on
line diff
--- a/demo/more/meta.urs	Mon Nov 02 14:22:29 2009 -0500
+++ b/demo/more/meta.urs	Mon Nov 02 15:48:06 2009 -0500
@@ -26,3 +26,11 @@
 
 val ensql : avail ::: {{Type}} -> ts ::: {(Type * Type)} -> $(map meta ts) -> $(map snd ts) -> folder ts
             -> $(map (sql_exp avail [] []) (map fst ts))
+
+con private = fn t :: Type =>
+                 {Nam : string,
+                  Initialize : t,
+                  Show : t -> xbody,
+                  Inject : sql_injectable t}
+
+val initialize : ts ::: {Type} -> $(map private ts) -> folder ts -> $(map (sql_exp [] [] []) ts)