|
23250
|
1 |
structure HOL =
|
|
|
2 |
struct
|
|
|
3 |
|
|
|
4 |
type 'a eq = {eq : 'a -> 'a -> bool};
|
|
|
5 |
fun eq (A_:'a eq) = #eq A_;
|
|
|
6 |
|
|
22386
|
7 |
type 'a ord = {less_eq : 'a -> 'a -> bool, less : 'a -> 'a -> bool};
|
|
|
8 |
fun less_eq (A_:'a ord) = #less_eq A_;
|
|
|
9 |
fun less (A_:'a ord) = #less A_;
|
|
21147
|
10 |
|
|
24193
|
11 |
end; (*struct HOL*)
|
|
21147
|
12 |
|
|
|
13 |
structure Codegen =
|
|
|
14 |
struct
|
|
|
15 |
|
|
23107
|
16 |
fun less_eq_product (A1_, A2_) B_ (x1, y1) (x2, y2) =
|
|
24193
|
17 |
HOL.less A2_ x1 x2 orelse HOL.eq A1_ x1 x2 andalso HOL.less_eq B_ y1 y2;
|
|
21147
|
18 |
|
|
|
19 |
end; (*struct Codegen*)
|