equal
deleted
inserted
replaced
1 structure Nat = |
1 structure Nat = |
2 struct |
2 struct |
3 |
3 |
4 datatype nat = Suc of nat | Zero_nat; |
4 datatype nat = Suc of nat | Zero_nat; |
5 |
5 |
6 fun eqop_nat Zero_nat (Suc m) = false |
6 fun eqop_nat Zero_nat Zero_nat = true |
7 | eqop_nat (Suc n) Zero_nat = false |
7 | eqop_nat (Suc m) (Suc n) = eqop_nat m n |
8 | eqop_nat (Suc n) (Suc m) = eqop_nat n m |
8 | eqop_nat Zero_nat (Suc a) = false |
9 | eqop_nat Zero_nat Zero_nat = true; |
9 | eqop_nat (Suc a) Zero_nat = false; |
10 |
10 |
11 fun plus_nat (Suc m) n = plus_nat m (Suc n) |
11 fun plus_nat (Suc m) n = plus_nat m (Suc n) |
12 | plus_nat Zero_nat n = n; |
12 | plus_nat Zero_nat n = n; |
13 |
13 |
14 end; (*struct Nat*) |
14 end; (*struct Nat*) |