diff src/elab_util.sig @ 211:e86411f647c6

Initial type class support
author Adam Chlipala <adamc@hcoop.net>
date Sat, 16 Aug 2008 14:32:18 -0400
parents ab86aa858e6c
children eec65c11d3e2
line wrap: on
line diff
--- a/src/elab_util.sig	Sat Aug 16 12:35:46 2008 -0400
+++ b/src/elab_util.sig	Sat Aug 16 14:32:18 2008 -0400
@@ -75,6 +75,11 @@
                    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