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.sig5
1 files changed, 5 insertions, 0 deletions
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,