pos_num

The type of positive binary numbers.

13 = 1101(base 2) = bit1 (bit0 (bit1 one))

num

The type of nonnegative binary numbers, using pos_num.

13 = 1101(base 2) = pos (bit1 (bit0 (bit1 one)))

znum

Representation of integers using trichotomy around zero.

13 = 1101(base 2) = pos (bit1 (bit0 (bit1 one)))
-13 = -1101(base 2) = neg (bit1 (bit0 (bit1 one)))

nzsnum

See snum.

snum

Alternative representation of integers using a sign bit at the end. The convention on sign here is to have the argument to msb denote the sign of the MSB itself, with all higher bits set to the negation of this sign. The result is interpreted in two's complement.

13  = ..0001101(base 2) = nz (bit1 (bit0 (bit1 (msb tt))))
-13 = ..1110011(base 2) = nz (bit1 (bit1 (bit0 (msb ff))))

As with num, a special case must be added for zero, which has no msb, but by two's complement symmetry there is a second special case for -1. Here the bool field indicates the sign of the number.

0  = ..0000000(base 2) = zero ff
-1 = ..1111111(base 2) = zero tt