1109 fun make_ord rel (x, y) = |
1109 fun make_ord rel (x, y) = |
1110 if rel (x, y) then LESS |
1110 if rel (x, y) then LESS |
1111 else if rel (y, x) then GREATER |
1111 else if rel (y, x) then GREATER |
1112 else EQUAL; |
1112 else EQUAL; |
1113 |
1113 |
1114 (*Better to use Int.compare*) |
1114 val int_ord = Int.compare; |
1115 fun int_ord (i, j: int) = |
1115 val string_ord = String.compare; |
1116 if i < j then LESS |
|
1117 else if i = j then EQUAL |
|
1118 else GREATER; |
|
1119 |
|
1120 (*Better to use String.compare*) |
|
1121 fun string_ord (a, b: string) = |
|
1122 if a < b then LESS |
|
1123 else if a = b then EQUAL |
|
1124 else GREATER; |
|
1125 |
1116 |
1126 (*lexicographic product*) |
1117 (*lexicographic product*) |
1127 fun prod_ord a_ord b_ord ((x, y), (x', y')) = |
1118 fun prod_ord a_ord b_ord ((x, y), (x', y')) = |
1128 (case a_ord (x, x') of EQUAL => b_ord (y, y') | ord => ord); |
1119 (case a_ord (x, x') of EQUAL => b_ord (y, y') | ord => ord); |
1129 |
1120 |