Negative Integer Literals - continued from Integers

There is a complication with negative integer literals; they are not implemented.

Although in theory (i.e., the theory in terms of which the semantics of the system is defined) each integer is represented as an atomic literal, we did not in fact implement negative literals. This complicates the rules for calculating with negative valued results somewhat.

The theoretical explanation of how to execute, e.g., m+n goes like this:

Execute the expressions m and n.
If the results are (atomic) integer literals, then return the integer literal corresponding to the sum.

The actual method of computation employed in proofs employs the non-canonical "-k" form, applied to a positive literal, in place of negative literals. Of course, the rules are still valid with respect to the theoretical execution method.

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html