Mercurial > urweb
comparison src/elab_util.sml @ 84:e86370850c30
Disjointness assumptions
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 01 Jul 2008 12:10:46 -0400 |
parents | b4f2a258e52c |
children | 1f85890c9846 |
comparison
equal
deleted
inserted
replaced
83:0a1baddd8ab2 | 84:e86370850c30 |
---|---|
122 S.bind2 (mfk k, | 122 S.bind2 (mfk k, |
123 fn k' => | 123 fn k' => |
124 S.map2 (mfc (bind (ctx, Rel (x, k))) c, | 124 S.map2 (mfc (bind (ctx, Rel (x, k))) c, |
125 fn c' => | 125 fn c' => |
126 (CAbs (x, k', c'), loc))) | 126 (CAbs (x, k', c'), loc))) |
127 | CDisjoint (c1, c2, c3) => | |
128 S.bind2 (mfc ctx c1, | |
129 fn c1' => | |
130 S.bind2 (mfc ctx c2, | |
131 fn c2' => | |
132 S.map2 (mfc ctx c3, | |
133 fn c3' => | |
134 (CDisjoint (c1', c2', c3'), loc)))) | |
127 | 135 |
128 | CName _ => S.return2 cAll | 136 | CName _ => S.return2 cAll |
129 | 137 |
130 | CRecord (k, xcs) => | 138 | CRecord (k, xcs) => |
131 S.bind2 (mfk k, | 139 S.bind2 (mfk k, |