summaryrefslogtreecommitdiff
path: root/lib/ur/top.ur
diff options
context:
space:
mode:
authorGravatar Benjamin Barenblat <bbaren@mit.edu>2016-10-23 14:26:59 -0400
committerGravatar Benjamin Barenblat <bbaren@mit.edu>2016-10-23 14:26:59 -0400
commit235602373c04aa38b7f8c93e6efbd9276ecc2266 (patch)
tree97c39e67902dd84d088ab930d8675e90760a674a /lib/ur/top.ur
parentc921d0df325c803fed8c7742eb088cb3d030d541 (diff)
parent20f3308b8c2a5a331239839e222bd21befde73eb (diff)
Merge branch 'upstream' into dfsg_clean20161022+dfsg
Diffstat (limited to 'lib/ur/top.ur')
-rw-r--r--lib/ur/top.ur7
1 files changed, 7 insertions, 0 deletions
diff --git a/lib/ur/top.ur b/lib/ur/top.ur
index 6c6c896c..02567917 100644
--- a/lib/ur/top.ur
+++ b/lib/ur/top.ur
@@ -179,6 +179,13 @@ fun mapUX [tf :: Type] [ctx :: {Unit}]
<xml>{f [nm] [rest] r}{acc}</xml>)
<xml/>
+fun mapUX_rev [tf :: Type] [ctx :: {Unit}]
+ (f : nm :: Name -> rest :: {Unit} -> [[nm] ~ rest] => tf -> xml ctx [] []) =
+ @@foldR [fn _ => tf] [fn _ => xml ctx [] []]
+ (fn [nm :: Name] [u :: Unit] [rest :: {Unit}] [[nm] ~ rest] r acc =>
+ <xml>{acc}{f [nm] [rest] r}</xml>)
+ <xml/>
+
fun mapX [K] [tf :: K -> Type] [ctx :: {Unit}]
(f : nm :: Name -> t :: K -> rest :: {K}
-> [[nm] ~ rest] =>