summaryrefslogtreecommitdiff
path: root/lib/ur/basis.urs
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-04-30 11:48:56 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-04-30 11:48:56 -0400
commit1a60a233b9349f320e67f35db1aa3b87d7c2a591 (patch)
tree3c14a4c191641933ffd1dc31c3d4d34535687368 /lib/ur/basis.urs
parent7a3ba5558cb363006aae188e02dd57dda833d356 (diff)
Subforms type-checks; lists urlified and unurlified
Diffstat (limited to 'lib/ur/basis.urs')
-rw-r--r--lib/ur/basis.urs13
1 files changed, 12 insertions, 1 deletions
diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs
index ea6f6f4a..117f944c 100644
--- a/lib/ur/basis.urs
+++ b/lib/ur/basis.urs
@@ -566,7 +566,18 @@ val subform : ctx ::: {Unit} -> use ::: {Type} -> bind ::: {Type}
nm :: Name -> [[nm] ~ use] =>
xml form [] bind
-> xml ([Form] ++ ctx) use [nm = $bind]
-
+
+val subforms : ctx ::: {Unit} -> use ::: {Type} -> bind ::: {Type}
+ -> [[Form] ~ ctx] =>
+ nm :: Name -> [[nm] ~ use] =>
+ xml [Body, Subform] [Entry = $bind] []
+ -> xml ([Form] ++ ctx) use [nm = list ($bind)]
+
+val entry : ctx ::: {Unit} -> bind ::: {Type}
+ -> [[Subform] ~ ctx] =>
+ xml form [] bind
+ -> xml ([Subform] ++ ctx) [Entry = $bind] []
+
con formTag = fn (ty :: Type) (inner :: {Unit}) (attrs :: {Type}) =>
ctx ::: {Unit}
-> [[Form] ~ ctx] =>