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