diff options
Diffstat (limited to 'lib/ur/top.ur')
-rw-r--r-- | lib/ur/top.ur | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/lib/ur/top.ur b/lib/ur/top.ur index 5d2ae606..79d30354 100644 --- a/lib/ur/top.ur +++ b/lib/ur/top.ur @@ -17,6 +17,18 @@ structure Folder = struct (f : nm :: Name -> v :: K -> r :: {K} -> tf r -> fn [[nm] ~ r] => tf ([nm = v] ++ r)) (i : tf []) = f [nm] [v] [r] (fold [tf] f i) + + fun concat K (r1 ::: {K}) (r2 ::: {K}) [r1 ~ r2] + (f1 : folder r1) (f2 : folder r2) + (tf :: {K} -> Type) + (f : nm :: Name -> v :: K -> r :: {K} -> tf r + -> fn [[nm] ~ r] => tf ([nm = v] ++ r)) + (i : tf []) = + f1 [fn r1' [r1' ~ r2] => tf (r1' ++ r2)] 0 + (*(fn (nm :: Name) (v :: K) (r1' :: {K}) (acc : fn [r1' ~ r2] => tf (r1' ++ r2)) + [[nm] ~ r1'] [[nm = v] ++ r1' ~ r2] => + f [nm] [v] [r1' ++ r2] acc) + (f2 [tf] f i)*) end |