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,