equal
deleted
inserted
replaced
1 structure HOL = |
|
2 struct |
|
3 |
|
4 datatype boola = False | True; |
|
5 |
|
6 fun anda x True = x |
|
7 | anda x False = False |
|
8 | anda True x = x |
|
9 | anda False x = False; |
|
10 |
|
11 end; (*struct HOL*) |
|
12 |
|
13 structure Nat = |
|
14 struct |
|
15 |
|
16 datatype nat = Suc of nat | Zero_nat; |
|
17 |
|
18 fun less_nat m (Suc n) = less_eq_nat m n |
|
19 | less_nat n Zero_nat = HOL.False |
|
20 and less_eq_nat (Suc m) n = less_nat m n |
|
21 | less_eq_nat Zero_nat n = HOL.True; |
|
22 |
|
23 end; (*struct Nat*) |
|
24 |
|
25 structure Codegen = |
|
26 struct |
|
27 |
|
28 fun in_interval (k, l) n = |
|
29 HOL.anda (Nat.less_eq_nat k n) (Nat.less_eq_nat n l); |
|
30 |
|
31 end; (*struct Codegen*) |
|