Mercurial > urweb

comparison src/elab_util.sig @ 76:522f4bd3955e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Broaden unification context
author Adam Chlipala <adamc@hcoop.net>
date Sun, 29 Jun 2008 10:39:43 -0400
parents abb2b32c19fb
children 8e9f97508f0d
comparison
equal deleted inserted replaced
75:88ffb3d61817 76:522f4bd3955e
105 sgn : Elab.sgn' -> Elab.sgn'} 105 sgn : Elab.sgn' -> Elab.sgn'}
106 -> Elab.sgn -> Elab.sgn 106 -> Elab.sgn -> Elab.sgn
107 107
108 end 108 end
109 109
110 structure Decl : sig
111 datatype binder =
112 RelC of string * Elab.kind
113 | NamedC of string * Elab.kind
114 | RelE of string * Elab.con
115 | NamedE of string * Elab.con
116 | Str of string * Elab.sgn
117 | Sgn of string * Elab.sgn
118
119 val mapfoldB : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder,
120 con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB,
121 exp : ('context, Elab.exp', 'state, 'abort) Search.mapfolderB,
122 sgn_item : ('context, Elab.sgn_item', 'state, 'abort) Search.mapfolderB,
123 sgn : ('context, Elab.sgn', 'state, 'abort) Search.mapfolderB,
124 str : ('context, Elab.str', 'state, 'abort) Search.mapfolderB,
125 decl : ('context, Elab.decl', 'state, 'abort) Search.mapfolderB,
126 bind : 'context * binder -> 'context}
127 -> ('context, Elab.decl, 'state, 'abort) Search.mapfolderB
128 val mapfold : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder,
129 con : (Elab.con', 'state, 'abort) Search.mapfolder,
130 exp : (Elab.exp', 'state, 'abort) Search.mapfolder,
131 sgn_item : (Elab.sgn_item', 'state, 'abort) Search.mapfolder,
132 sgn : (Elab.sgn', 'state, 'abort) Search.mapfolder,
133 str : (Elab.str', 'state, 'abort) Search.mapfolder,
134 decl : (Elab.decl', 'state, 'abort) Search.mapfolder}
135 -> (Elab.decl, 'state, 'abort) Search.mapfolder
136 val exists : {kind : Elab.kind' -> bool,
137 con : Elab.con' -> bool,
138 exp : Elab.exp' -> bool,
139 sgn_item : Elab.sgn_item' -> bool,
140 sgn : Elab.sgn' -> bool,
141 str : Elab.str' -> bool,
142 decl : Elab.decl' -> bool}
143 -> Elab.decl -> bool
144 val search : {kind : Elab.kind' -> 'a option,
145 con : Elab.con' -> 'a option,
146 exp : Elab.exp' -> 'a option,
147 sgn_item : Elab.sgn_item' -> 'a option,
148 sgn : Elab.sgn' -> 'a option,
149 str : Elab.str' -> 'a option,
150 decl : Elab.decl' -> 'a option}
151 -> Elab.decl -> 'a option
110 end 152 end
153
154 end