| changeset 9509 | 0f3ee1f89ca8 |
| parent 7032 | d6efb3b8e669 |
| child 10574 | 8f98f0301d67 |
| 9508:4d01dbf6ded7 | 9509:0f3ee1f89ca8 |
|---|---|
6 Binary arithmetic for the natural numbers |
6 Binary arithmetic for the natural numbers |
7 |
7 |
8 This case is simply reduced to that for the non-negative integers |
8 This case is simply reduced to that for the non-negative integers |
9 *) |
9 *) |
10 |
10 |
11 NatBin = IntDiv + |
11 NatBin = IntPower + |
12 |
12 |
13 instance |
13 instance |
14 nat :: number |
14 nat :: number |
15 |
15 |
16 defs |
16 defs |