Mercurial > urweb
comparison src/elab_util.sml @ 85:1f85890c9846
Disjointness assumptions in expressions
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 01 Jul 2008 12:25:12 -0400 |
parents | e86370850c30 |
children | 7bab29834cd6 |
comparison
equal
deleted
inserted
replaced
84:e86370850c30 | 85:1f85890c9846 |
---|---|
102 S.bind2 (mfk k, | 102 S.bind2 (mfk k, |
103 fn k' => | 103 fn k' => |
104 S.map2 (mfc (bind (ctx, Rel (x, k))) c, | 104 S.map2 (mfc (bind (ctx, Rel (x, k))) c, |
105 fn c' => | 105 fn c' => |
106 (TCFun (e, x, k', c'), loc))) | 106 (TCFun (e, x, k', c'), loc))) |
107 | TDisjoint (c1, c2, c3) => | |
108 S.bind2 (mfc ctx c1, | |
109 fn c1' => | |
110 S.bind2 (mfc ctx c2, | |
111 fn c2' => | |
112 S.map2 (mfc ctx c3, | |
113 fn c3' => | |
114 (TDisjoint (c1', c2', c3'), loc)))) | |
107 | TRecord c => | 115 | TRecord c => |
108 S.map2 (mfc ctx c, | 116 S.map2 (mfc ctx c, |
109 fn c' => | 117 fn c' => |
110 (TRecord c', loc)) | 118 (TRecord c', loc)) |
111 | 119 |