Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
to their abstract counterparts, while other binary numerals work correctly.
Defs = Types +
consts nand, exor :: gate
defs nand_def "nand A B == ~(A & B)"
exor_def "exor A B == A & ~B | ~A & B"
end