Mercurial > urweb

comparison src/elab_util.sml @ 82:b4f2a258e52c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Initial disjointness prover
author Adam Chlipala <adamc@hcoop.net>
date Tue, 01 Jul 2008 10:55:38 -0400
parents 522f4bd3955e
children e86370850c30
comparison
equal deleted inserted replaced
81:60d97de1bbe8 82:b4f2a258e52c
54 | KRecord k => 54 | KRecord k =>
55 S.map2 (mfk k, 55 S.map2 (mfk k,
56 fn k' => 56 fn k' =>
57 (KRecord k', loc)) 57 (KRecord k', loc))
58 58
59 | KUnit => S.return2 kAll
60
59 | KError => S.return2 kAll 61 | KError => S.return2 kAll
60 62
61 | KUnif (_, _, ref (SOME k)) => mfk' k 63 | KUnif (_, _, ref (SOME k)) => mfk' k
62 | KUnif _ => S.return2 kAll 64 | KUnif _ => S.return2 kAll
63 in 65 in
147 S.bind2 (mfk k1, 149 S.bind2 (mfk k1,
148 fn k1' => 150 fn k1' =>
149 S.map2 (mfk k2, 151 S.map2 (mfk k2,
150 fn k2' => 152 fn k2' =>
151 (CFold (k1', k2'), loc))) 153 (CFold (k1', k2'), loc)))
154
155 | CUnit => S.return2 cAll
152 156
153 | CError => S.return2 cAll 157 | CError => S.return2 cAll
154 | CUnif (_, _, _, ref (SOME c)) => mfc' ctx c 158 | CUnif (_, _, _, ref (SOME c)) => mfc' ctx c
155 | CUnif _ => S.return2 cAll 159 | CUnif _ => S.return2 cAll
156 in 160 in