aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/ur
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-03-10 16:38:38 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-03-10 16:38:38 -0400
commit4bc363c5ec2724b9d310e17181ca87517c98aa68 (patch)
treec0dff25071f38e045374e6d001ef7356af04e5db /lib/ur
parentb8e7b835e7cde4cf374138467da8b16e93a65eb9 (diff)
BatchG demo
Diffstat (limited to 'lib/ur')
-rw-r--r--lib/ur/top.ur2
-rw-r--r--lib/ur/top.urs2
2 files changed, 2 insertions, 2 deletions
diff --git a/lib/ur/top.ur b/lib/ur/top.ur
index f4adaba7..2ae424ab 100644
--- a/lib/ur/top.ur
+++ b/lib/ur/top.ur
@@ -7,7 +7,7 @@ con folder = K ==> fn r :: {K} =>
-> tf [] -> tf r
structure Folder = struct
- fun fold K (r ::: {K}) (fl : folder r) = fl
+ fun fold K (r :: {K}) (fl : folder r) = fl
fun nil K (tf :: {K} -> Type)
(f : nm :: Name -> v :: K -> r :: {K} -> tf r
diff --git a/lib/ur/top.urs b/lib/ur/top.urs
index bb85abd0..009a4ed5 100644
--- a/lib/ur/top.urs
+++ b/lib/ur/top.urs
@@ -3,7 +3,7 @@
con folder :: K --> {K} -> Type
structure Folder : sig
- val fold : K --> r ::: {K} -> folder r
+ val fold : K --> r :: {K} -> folder r
-> tf :: ({K} -> Type)
-> (nm :: Name -> v :: K -> r :: {K} -> tf r
-> [[nm] ~ r] => tf ([nm = v] ++ r))