Mercurial > urweb
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