summaryrefslogtreecommitdiff
path: root/src/elab_util.sig
diff options
context:
space:
mode:
Diffstat (limited to 'src/elab_util.sig')
-rw-r--r--src/elab_util.sig4
1 files changed, 4 insertions, 0 deletions
diff --git a/src/elab_util.sig b/src/elab_util.sig
index 817f885f..5b4bc46a 100644
--- a/src/elab_util.sig
+++ b/src/elab_util.sig
@@ -62,6 +62,10 @@ structure Con : sig
val map : {kind : Elab.kind' -> Elab.kind',
con : Elab.con' -> Elab.con'}
-> Elab.con -> Elab.con
+ val existsB : {kind : 'context * Elab.kind' -> bool,
+ con : 'context * Elab.con' -> bool,
+ bind : 'context * binder -> 'context}
+ -> 'context -> Elab.con -> bool
val exists : {kind : Elab.kind' -> bool,
con : Elab.con' -> bool} -> Elab.con -> bool