Lines Matching defs:cmp
196 fun cmp Axiom Axiom = EQUAL
197 | cmp Axiom _ = LESS
198 | cmp _ Axiom = GREATER
199 | cmp Refl Refl = EQUAL
200 | cmp Refl _ = LESS
201 | cmp _ Refl = GREATER
202 | cmp Assume Assume = EQUAL
203 | cmp Assume _ = LESS
204 | cmp _ Assume = GREATER
205 | cmp Inst Inst = EQUAL
206 | cmp Inst _ = LESS
207 | cmp _ Inst = GREATER
208 | cmp Factor Factor = EQUAL
209 | cmp Factor _ = LESS
210 | cmp _ Factor = GREATER
211 | cmp Resolve Resolve = EQUAL
212 | cmp Resolve Equality = LESS
213 | cmp Equality Resolve = GREATER
214 | cmp Equality Equality = EQUAL;
224 => (case cmp p1 p2 of EQUAL => cm (zip ths1 ths2 @ l) | x => x)