diff src/elab_util.sml @ 1795:d28adceef22a

Allow type class instances with hypotheses via local ('let') definitions
author Adam Chlipala <adam@chlipala.net>
date Wed, 25 Jul 2012 14:04:59 -0400
parents 4a03aa3251cb
children bb942416bf1c
line wrap: on
line diff
--- a/src/elab_util.sml	Wed Jul 25 08:20:15 2012 -0400
+++ b/src/elab_util.sml	Wed Jul 25 14:04:59 2012 -0400
@@ -568,6 +568,26 @@
               exp = fn () => fe,
               bind = fn ((), _) => ()} ()
 
+fun existsB {kind, con, exp, bind} ctx e =
+    case mapfoldB {kind = fn ctx => fn k => fn () =>
+                                               if kind (ctx, k) then
+                                                   S.Return ()
+                                               else
+                                                   S.Continue (k, ()),
+                   con = fn ctx => fn c => fn () =>
+                                              if con (ctx, c) then
+                                                  S.Return ()
+                                              else
+                                                  S.Continue (c, ()),
+                   exp = fn ctx => fn e => fn () =>
+                                              if exp (ctx, e) then
+                                                  S.Return ()
+                                              else
+                                                  S.Continue (e, ()),
+                   bind = bind} ctx e () of
+        S.Return _ => true
+      | S.Continue _ => false
+
 fun exists {kind, con, exp} k =
     case mapfold {kind = fn k => fn () =>
                                     if kind k then