diff src/elab_util.sml @ 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 22117edf8fd3
children
line wrap: on
line diff
--- a/src/elab_util.sml	Tue Dec 15 19:58:52 2015 -0500
+++ b/src/elab_util.sml	Sun Dec 20 13:41:35 2015 -0500
@@ -116,6 +116,12 @@
         S.Return _ => true
       | S.Continue _ => false
 
+fun foldB {kind, bind} ctx st k =
+    case mapfoldB {kind = fn ctx => fn k => fn st => S.Continue (k, kind (ctx, k, st)),
+                   bind = bind} ctx k st of
+        S.Continue (_, st) => st
+      | S.Return _ => raise Fail "ElabUtil.Kind.foldB: Impossible"
+
 end
 
 val mliftConInCon = ref (fn n : int => fn c : con => (raise Fail "You didn't set ElabUtil.mliftConInCon!") : con)