changeset 22015 | 12b94d7f7e1f |
parent 21994 | dfa5133dbe73 |
child 22386 | 4ebe883b02ff |
22014:4b70cbd96007 | 22015:12b94d7f7e1f |
---|---|
24 |
24 |
25 structure Codegen = |
25 structure Codegen = |
26 struct |
26 struct |
27 |
27 |
28 fun in_interval (k, l) n = |
28 fun in_interval (k, l) n = |
29 (Nat.less_eq_nat k n andalso Nat.less_eq_nat n l); |
29 Nat.less_eq_nat k n andalso Nat.less_eq_nat n l; |
30 |
30 |
31 end; (*struct Codegen*) |
31 end; (*struct Codegen*) |
32 |
32 |
33 end; (*struct ROOT*) |
33 end; (*struct ROOT*) |