Mercurial > urweb
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