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.sig7
1 files changed, 7 insertions, 0 deletions
diff --git a/src/elab_util.sig b/src/elab_util.sig
index 2998e7db..8a013554 100644
--- a/src/elab_util.sig
+++ b/src/elab_util.sig
@@ -64,6 +64,13 @@ structure Con : sig
val map : {kind : Elab.kind' -> Elab.kind',
con : Elab.con' -> Elab.con'}
-> Elab.con -> Elab.con
+ val appB : {kind : 'context -> Elab.kind' -> unit,
+ con : 'context -> Elab.con' -> unit,
+ bind : 'context * binder -> 'context}
+ -> 'context -> (Elab.con -> unit)
+ val app : {kind : Elab.kind' -> unit,
+ con : Elab.con' -> unit}
+ -> Elab.con -> unit
val existsB : {kind : 'context * Elab.kind' -> bool,
con : 'context * Elab.con' -> bool,
bind : 'context * binder -> 'context}