author | haftmann |
Fri, 24 Aug 2007 14:14:17 +0200 | |
changeset 24421 | acfb2413faa3 |
parent 24193 | 926dde4d96de |
child 26513 | 6f306c8c2c54 |
permissions | -rw-r--r-- |
structure HOL = struct type 'a eq = {eqop : 'a -> 'a -> bool}; fun eqop (A_:'a eq) = #eqop A_; type 'a ord = {less_eq : 'a -> 'a -> bool, less : 'a -> 'a -> bool}; fun less_eq (A_:'a ord) = #less_eq A_; fun less (A_:'a ord) = #less A_; end; (*struct HOL*) structure Codegen = struct fun less_eq (A1_, A2_) B_ (x1, y1) (x2, y2) = HOL.less A2_ x1 x2 orelse HOL.eqop A1_ x1 x2 andalso HOL.less_eq B_ y1 y2; end; (*struct Codegen*)