Mercurial > urweb

diff lib/ur/top.urs @ 628:12b73f3c108e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Switch to TDisjoint from CDisjoint; still need to implement obligation generation at EDisjoint uses
author Adam Chlipala <adamc@hcoop.net>
date Tue, 24 Feb 2009 12:01:24 -0500
parents f4f2b09a533a
children e68de2a5506b
line wrap: on
line diff
--- a/lib/ur/top.urs	Sun Feb 22 17:39:55 2009 -0500
+++ b/lib/ur/top.urs	Tue Feb 24 12:01:24 2009 -0500
@@ -10,6 +10,8 @@
     val nil : K --> folder (([]) :: {K})
     val cons : K --> r ::: {K} -> nm :: Name -> v :: K
                -> fn [[nm] ~ r] => folder r -> folder ([nm = v] ++ r)
+    val concat : K --> r1 ::: {K} -> r2 ::: {K}
+                 -> fn [r1 ~ r2] => folder r1 -> folder r2 -> folder (r1 ++ r2)
 end