summaryrefslogtreecommitdiff
path: root/src/elab_util.sml
diff options
context:
space:
mode:
Diffstat (limited to 'src/elab_util.sml')
-rw-r--r--src/elab_util.sml6
1 files changed, 6 insertions, 0 deletions
diff --git a/src/elab_util.sml b/src/elab_util.sml
index acc696dd..ed2e82a0 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -116,6 +116,12 @@ fun exists f k =
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)