summaryrefslogtreecommitdiff
path: root/src/elab_util.sig
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2012-07-25 14:04:59 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2012-07-25 14:04:59 -0400
commitb2f6e6a5501937c58cbd8eb9b5d90ceae0321386 (patch)
tree65d3f936aeb2cb122bc23fcccb19aa571b296fc7 /src/elab_util.sig
parent041a250016b69a70a1fa1ab91ef3c2e61908a9db (diff)
Allow type class instances with hypotheses via local ('let') definitions
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,