author | haftmann |
Tue, 05 Jun 2007 15:16:11 +0200 | |
changeset 23250 | 9886802cbbd6 |
parent 23107 | 0c3c55b7c98f |
child 23850 | f1434532a562 |
permissions | -rw-r--r-- |
21147 | 1 |
structure ROOT = |
2 |
struct |
|
3 |
||
23250 | 4 |
structure HOL = |
5 |
struct |
|
6 |
||
7 |
type 'a eq = {eq : 'a -> 'a -> bool}; |
|
8 |
fun eq (A_:'a eq) = #eq A_; |
|
9 |
||
10 |
end; (*struct HOL*) |
|
11 |
||
21147 | 12 |
structure Orderings = |
13 |
struct |
|
14 |
||
22386 | 15 |
type 'a ord = {less_eq : 'a -> 'a -> bool, less : 'a -> 'a -> bool}; |
16 |
fun less_eq (A_:'a ord) = #less_eq A_; |
|
17 |
fun less (A_:'a ord) = #less A_; |
|
21147 | 18 |
|
19 |
end; (*struct Orderings*) |
|
20 |
||
21 |
structure Codegen = |
|
22 |
struct |
|
23 |
||
23107 | 24 |
fun less_eq_product (A1_, A2_) B_ (x1, y1) (x2, y2) = |
22188
a63889770d57
adjusted manual to improved treatment of overloaded constants
haftmann
parents:
22015
diff
changeset
|
25 |
Orderings.less A2_ x1 x2 orelse |
23250 | 26 |
HOL.eq A1_ x1 x2 andalso Orderings.less_eq B_ y1 y2; |
21147 | 27 |
|
28 |
end; (*struct Codegen*) |
|
29 |
||
30 |
end; (*struct ROOT*) |