Lines Matching defs:cm
450 fun cm [] = EQUAL
451 | cm ((True, True ) :: l) = cm l
452 | cm ((True, _ ) :: _) = LESS
453 | cm ((_, True ) :: _) = GREATER
454 | cm ((False, False ) :: l) = cm l
455 | cm ((False, _ ) :: _) = LESS
456 | cm ((_, False ) :: _) = GREATER
457 | cm ((Atom t, Atom u ) :: l) = lex (cmt [(t, u)]) cm l
458 | cm ((Atom _, _ ) :: _) = LESS
459 | cm ((_, Atom _ ) :: _) = GREATER
460 | cm ((Not p, Not q ) :: l) = cm ((p, q) :: l)
461 | cm ((Not _ , _ ) :: _) = LESS
462 | cm ((_, Not _ ) :: _) = GREATER
463 | cm ((And (p1, q1), And (p2, q2) ) :: l) = cm ((p1, p2) :: (q1, q2) :: l)
464 | cm ((And _, _ ) :: _) = LESS
465 | cm ((_, And _ ) :: _) = GREATER
466 | cm ((Or (p1, q1), Or (p2, q2) ) :: l) = cm ((p1, p2) :: (q1, q2) :: l)
467 | cm ((Or _, _ ) :: _) = LESS
468 | cm ((_, Or _ ) :: _) = GREATER
469 | cm ((Imp (p1, q1), Imp (p2, q2) ) :: l) = cm ((p1, p2) :: (q1, q2) :: l)
470 | cm ((Imp _, _ ) :: _) = LESS
471 | cm ((_, Imp _ ) :: _) = GREATER
472 | cm ((Iff (p1, q1), Iff (p2, q2) ) :: l) = cm ((p1, p2) :: (q1, q2) :: l)
473 | cm ((Iff _, _ ) :: _) = LESS
474 | cm ((_, Iff _ ) :: _) = GREATER
475 | cm ((Forall (v, p), Forall (w, q)) :: l) =
476 lex (String.compare (v, w)) (cm o cons (p, q)) l
477 | cm ((Forall _, Exists _ ) :: _) = LESS
478 | cm ((Exists _, Forall _ ) :: _) = GREATER
479 | cm ((Exists (v, p), Exists (w, q)) :: l) =
480 lex (String.compare (v, w)) (cm o cons (p, q)) l;
483 val formula_compare = cm o sing;