Mercurial > urweb
diff lib/ur/top.urs @ 653:e5894f0e541a
Change location/type of [fold] to be more uniform w.r.t. derived folders
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Thu, 12 Mar 2009 10:26:04 -0400 |
parents | fcf0bd3d1667 |
children | 5bbb542243e8 |
line wrap: on
line diff
--- a/lib/ur/top.urs Thu Mar 12 10:16:59 2009 -0400 +++ b/lib/ur/top.urs Thu Mar 12 10:26:04 2009 -0400 @@ -2,13 +2,13 @@ con folder :: K --> {K} -> Type +val fold : K --> tf :: ({K} -> Type) + -> (nm :: Name -> v :: K -> r :: {K} -> [[nm] ~ r] => + tf r -> tf ([nm = v] ++ r)) + -> tf [] + -> r :: {K} -> folder r -> tf r + structure Folder : sig - val fold : K --> r :: {K} -> folder r - -> tf :: ({K} -> Type) - -> (nm :: Name -> v :: K -> r :: {K} -> tf r - -> [[nm] ~ r] => tf ([nm = v] ++ r)) - -> tf [] -> tf r - val nil : K --> folder (([]) :: {K}) val cons : K --> r ::: {K} -> nm :: Name -> v :: K -> [[nm] ~ r] => folder r -> folder ([nm = v] ++ r)