diff src/elab_util.sig @ 2201:1091227f535a

Unnest properly in presence of kind polymorphism
author Adam Chlipala <adam@chlipala.net>
date Sun, 20 Dec 2015 13:41:35 -0500
parents d28adceef22a
children
line wrap: on
line diff
--- a/src/elab_util.sig	Tue Dec 15 19:58:52 2015 -0500
+++ b/src/elab_util.sig	Sun Dec 20 13:41:35 2015 -0500
@@ -41,6 +41,9 @@
     val mapB : {kind : 'context -> Elab.kind' -> Elab.kind',
                 bind : 'context * string -> 'context}
                -> 'context -> (Elab.kind -> Elab.kind)
+    val foldB : {kind : 'context * Elab.kind' * 'state -> 'state,
+                 bind : 'context * string -> 'context}
+                -> 'context -> 'state -> Elab.kind -> 'state
 end
 
 structure Con : sig