comparison 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
comparison
equal deleted inserted replaced
9:14b533dbe6cc 10:dde5c52e5e5e
33 val exists : (Elab.kind' -> bool) -> Elab.kind -> bool 33 val exists : (Elab.kind' -> bool) -> Elab.kind -> bool
34 end 34 end
35 35
36 structure Con : sig 36 structure Con : sig
37 val mapfold : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder, 37 val mapfold : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder,
38 con : (Elab.con', 'state, 'abort) Search.mapfolder} 38 con : (Elab.con', 'state, 'abort) Search.mapfolder}
39 -> (Elab.con, 'state, 'abort) Search.mapfolder 39 -> (Elab.con, 'state, 'abort) Search.mapfolder
40 val exists : {kind : Elab.kind' -> bool, 40 val exists : {kind : Elab.kind' -> bool,
41 con : Elab.con' -> bool} -> Elab.con -> bool 41 con : Elab.con' -> bool} -> Elab.con -> bool
42 end 42 end
43 43
44 structure Exp : sig
45 val mapfold : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder,
46 con : (Elab.con', 'state, 'abort) Search.mapfolder,
47 exp : (Elab.exp', 'state, 'abort) Search.mapfolder}
48 -> (Elab.exp, 'state, 'abort) Search.mapfolder
49 val exists : {kind : Elab.kind' -> bool,
50 con : Elab.con' -> bool,
51 exp : Elab.exp' -> bool} -> Elab.exp -> bool
52 end
53
44 val declBinds : ElabEnv.env -> Elab.decl -> ElabEnv.env 54 val declBinds : ElabEnv.env -> Elab.decl -> ElabEnv.env
45 55
46 end 56 end