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