diff options
author | Adam Chlipala <adamc@hcoop.net> | 2009-02-24 13:50:39 -0500 |
---|---|---|
committer | Adam Chlipala <adamc@hcoop.net> | 2009-02-24 13:50:39 -0500 |
commit | 7325b2f19498583eb190a70cb789dfd3e305273b (patch) | |
tree | 84b91f76ce37f9fb6245d9040c9641188968f729 /lib/ur/top.ur | |
parent | ee3f3e9e0a82141b6831b22d4f1412f5a9fb91d4 (diff) |
Top.Fold.mp
Diffstat (limited to 'lib/ur/top.ur')
-rw-r--r-- | lib/ur/top.ur | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/lib/ur/top.ur b/lib/ur/top.ur index 0fca0a5b..5ce6ea9a 100644 --- a/lib/ur/top.ur +++ b/lib/ur/top.ur @@ -29,6 +29,17 @@ structure Folder = struct [[nm] ~ r1'] [[nm = v] ++ r1' ~ r2] => f [nm] [v] [r1' ++ r2] acc !) (fn [[] ~ r2] => f2 [tf] f i) ! + + fun mp K1 K2 (f ::: K1 -> K2) (r ::: {K1}) + (fold : folder r) + (tf :: {K2} -> Type) + (f : nm :: Name -> v :: K2 -> r :: {K2} -> tf r + -> [[nm] ~ r] => tf ([nm = v] ++ r)) + (i : tf []) = + fold [fn r => tf (map f r)] + (fn (nm :: Name) (v :: K1) (rest :: {K1}) (acc : tf (map f rest)) [[nm] ~ rest] => + f [nm] [f v] [map f rest] acc !) + i end |