diff src/elab_util.sig @ 10:dde5c52e5e5e

Start of elaborating expressions
author Adam Chlipala <adamc@hcoop.net>
date Fri, 28 Mar 2008 13:59:03 -0400
parents 38bf996e1c2e
children e97c6d335869
line wrap: on
line diff
--- a/src/elab_util.sig	Sat Jan 26 17:26:14 2008 -0500
+++ b/src/elab_util.sig	Fri Mar 28 13:59:03 2008 -0400
@@ -35,12 +35,22 @@
 
 structure Con : sig
     val mapfold : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder,
-                      con : (Elab.con', 'state, 'abort) Search.mapfolder}
+                   con : (Elab.con', 'state, 'abort) Search.mapfolder}
                   -> (Elab.con, 'state, 'abort) Search.mapfolder
     val exists : {kind : Elab.kind' -> bool,
                   con : Elab.con' -> bool} -> Elab.con -> bool
 end
 
+structure Exp : sig
+    val mapfold : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder,
+                   con : (Elab.con', 'state, 'abort) Search.mapfolder,
+                   exp : (Elab.exp', 'state, 'abort) Search.mapfolder}
+                  -> (Elab.exp, 'state, 'abort) Search.mapfolder
+    val exists : {kind : Elab.kind' -> bool,
+                  con : Elab.con' -> bool,
+                  exp : Elab.exp' -> bool} -> Elab.exp -> bool
+end
+
 val declBinds : ElabEnv.env -> Elab.decl -> ElabEnv.env
 
 end