equal
deleted
inserted
replaced
|
1 structure HOL = |
|
2 struct |
|
3 |
|
4 fun leta s f = f s; |
|
5 |
|
6 end; (*struct HOL*) |
|
7 |
1 structure Nat = |
8 structure Nat = |
2 struct |
9 struct |
3 |
10 |
4 datatype nat = Zero_nat | Suc of nat; |
11 datatype nat = Zero_nat | Suc of nat; |
5 |
12 |
9 | less_eq_nat Zero_nat m = true; |
16 | less_eq_nat Zero_nat m = true; |
10 |
17 |
11 fun minus_nat (Suc m) (Suc n) = minus_nat m n |
18 fun minus_nat (Suc m) (Suc n) = minus_nat m n |
12 | minus_nat Zero_nat n = Zero_nat |
19 | minus_nat Zero_nat n = Zero_nat |
13 | minus_nat m Zero_nat = m; |
20 | minus_nat m Zero_nat = m; |
|
21 |
|
22 fun prod_case f1 (a, b) = f1 a b; |
14 |
23 |
15 end; (*struct Nat*) |
24 end; (*struct Nat*) |
16 |
25 |
17 structure Codegen = |
26 structure Codegen = |
18 struct |
27 struct |