Mercurial > urweb

diff src/elab_util.sig @ 1795:d28adceef22a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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 1091227f535a
line wrap: on
line diff
--- a/src/elab_util.sig	Wed Jul 25 08:20:15 2012 -0400
+++ b/src/elab_util.sig	Wed Jul 25 14:04:59 2012 -0400
@@ -112,6 +112,11 @@
     val exists : {kind : Elab.kind' -> bool,
                   con : Elab.con' -> bool,
                   exp : Elab.exp' -> bool} -> Elab.exp -> bool
+    val existsB : {kind : 'context * Elab.kind' -> bool,
+                   con : 'context * Elab.con' -> bool,
+                   exp : 'context * Elab.exp' -> bool,
+                   bind : 'context * binder -> 'context}
+                  -> 'context -> Elab.exp -> bool
 
     val foldB : {kind : 'context * Elab.kind' * 'state -> 'state,
                  con : 'context * Elab.con' * 'state -> 'state,