| changeset 30228 | 2aaf339fb7c1 |
| parent 30224 | 79136ce06bdb |
| parent 30227 | 853abb4853cc |
| child 30229 | 9861257b18e6 |
| child 30243 | 09d5944e224e |
| 30224:79136ce06bdb | 30228:2aaf339fb7c1 |
|---|---|
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*) |