| changeset 30226 | 2f4684e2ea95 |
| parent 30202 | 2775062fd3a9 |
| child 30227 | 853abb4853cc |
| 30202:2775062fd3a9 | 30226:2f4684e2ea95 |
|---|---|
1 structure HOL = |
|
2 struct |
|
3 |
|
4 type 'a eq = {eq : 'a -> 'a -> bool}; |
|
5 fun eq (A_:'a eq) = #eq A_; |
|
6 |
|
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_; |
|
10 |
|
11 end; (*struct HOL*) |
|
12 |
|
13 structure Codegen = |
|
14 struct |
|
15 |
|
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; |
|
18 |
|
19 end; (*struct Codegen*) |