### -

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).