From 7c37a6336fb1a56fee80e94f9e5188c3436102cd Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Wed, 25 Jul 2012 14:04:59 -0400
Subject: Allow type class instances with hypotheses via local ('let')
 definitions

---
 src/elab_util.sig | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'src/elab_util.sig')

diff --git a/src/elab_util.sig b/src/elab_util.sig
index b63d9b7f..6c08442b 100644
--- a/src/elab_util.sig
+++ b/src/elab_util.sig
@@ -112,6 +112,11 @@ structure Exp : sig
     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,
-- 
cgit v1.2.3