changeset 30242 | aea5d7fa7ef5 |
parent 26318 | 967323f93c67 |
30241:3a1aef73b2b2 | 30242:aea5d7fa7ef5 |
---|---|
1 structure Nat = |
|
2 struct |
|
3 |
|
4 datatype nat = Suc of nat | Zero_nat; |
|
5 |
|
6 fun less_nat m (Suc n) = less_eq_nat m n |
|
7 | less_nat n Zero_nat = false |
|
8 and less_eq_nat (Suc m) n = less_nat m n |
|
9 | less_eq_nat Zero_nat n = true; |
|
10 |
|
11 end; (*struct Nat*) |
|
12 |
|
13 structure Codegen = |
|
14 struct |
|
15 |
|
16 fun in_interval (k, l) n = |
|
17 Nat.less_eq_nat k n andalso Nat.less_eq_nat n l; |
|
18 |
|
19 end; (*struct Codegen*) |