comparison src/elaborate.sml @ 9:14b533dbe6cc

Added simple expression constructors to Elab
author Adam Chlipala <adamc@hcoop.net>
date Sat, 26 Jan 2008 17:26:14 -0500
parents a455a9f85cc3
children dde5c52e5e5e
comparison
equal deleted inserted replaced
8:a455a9f85cc3 9:14b533dbe6cc
199 ((L'.TRecord c', loc), ktype) 199 ((L'.TRecord c', loc), ktype)
200 end 200 end
201 201
202 | L.CVar s => 202 | L.CVar s =>
203 (case E.lookupC env s of 203 (case E.lookupC env s of
204 E.CNotBound => 204 E.NotBound =>
205 (conError env (UnboundCon (loc, s)); 205 (conError env (UnboundCon (loc, s));
206 (cerror, kerror)) 206 (cerror, kerror))
207 | E.CRel (n, k) => 207 | E.Rel (n, k) =>
208 ((L'.CRel n, loc), k) 208 ((L'.CRel n, loc), k)
209 | E.CNamed (n, k) => 209 | E.Named (n, k) =>
210 ((L'.CNamed n, loc), k)) 210 ((L'.CNamed n, loc), k))
211 | L.CApp (c1, c2) => 211 | L.CApp (c1, c2) =>
212 let 212 let
213 val (c1', k1) = elabCon env c1 213 val (c1', k1) = elabCon env c1
214 val (c2', k2) = elabCon env c2 214 val (c2', k2) = elabCon env c2