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