aboutsummaryrefslogtreecommitdiffhomepage
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 e33e956b..57883073 100644
--- a/src/elab_util.sig
+++ b/src/elab_util.sig
@@ -75,6 +75,11 @@ structure Exp : sig
con : (Elab.con', 'state, 'abort) Search.mapfolder,
exp : (Elab.exp', 'state, 'abort) Search.mapfolder}
-> (Elab.exp, 'state, 'abort) Search.mapfolder
+ val mapB : {kind : Elab.kind' -> Elab.kind',
+ con : 'context -> Elab.con' -> Elab.con',
+ exp : 'context -> Elab.exp' -> Elab.exp',
+ bind : 'context * binder -> 'context}
+ -> 'context -> (Elab.exp -> Elab.exp)
val exists : {kind : Elab.kind' -> bool,
con : Elab.con' -> bool,
exp : Elab.exp' -> bool} -> Elab.exp -> bool