-

macro for subtraction and negation
Major Section:  ACL2-BUILT-INS

See binary-+ for addition and see unary-- for negation.

Note that - represents subtraction as follows:

(- x y)
represents the same term as
(+ x (- y))
which is really
(binary-+ x (unary-- y)).
Also note that - represents arithmetic negation as follows:
(- x)
expands to
(unary-- x).