diff lib/ur/top.ur @ 631:effa7d43aac3

Make folders abstract
author Adam Chlipala <adamc@hcoop.net>
date Tue, 24 Feb 2009 14:04:07 -0500
parents 6a6eb9882d57
children 6c4643880df5
line wrap: on
line diff
--- a/lib/ur/top.ur	Tue Feb 24 13:50:39 2009 -0500
+++ b/lib/ur/top.ur	Tue Feb 24 14:04:07 2009 -0500
@@ -7,6 +7,8 @@
                       -> tf [] -> tf r
 
 structure Folder = struct
+    fun fold K (r ::: {K}) (fl : folder r) = fl
+
     fun nil K (tf :: {K} -> Type)
             (f : nm :: Name -> v :: K -> r :: {K} -> tf r
                  -> [[nm] ~ r] => tf ([nm = v] ++ r))