diff options
| author |  Adam Chlipala <adam@chlipala.net> | 2012-07-25 14:04:59 -0400 |
|---|---|---|
| committer | Adam Chlipala <adam@chlipala.net> | 2012-07-25 14:04:59 -0400 |
| commit | 7c37a6336fb1a56fee80e94f9e5188c3436102cd (patch) | |
| tree | 65d3f936aeb2cb122bc23fcccb19aa571b296fc7 /src/elab_util.sml | |
| parent | 59fbe515a0462e98ab3cbb78a1f136f382ab927a (diff) | |
Allow type class instances with hypotheses via local ('let') definitions
Diffstat (limited to 'src/elab_util.sml')
| -rw-r--r-- | src/elab_util.sml | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/src/elab_util.sml b/src/elab_util.sml index b799bbc4..97e3b572 100644 --- a/src/elab_util.sml +++ b/src/elab_util.sml @@ -568,6 +568,26 @@ fun mapfold {kind = fk, con = fc, exp = fe} = 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 |