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