		Search-engine friendly clone of the ACL2 documentation.

-

Macro for subtraction and negation

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

Macro: -

(defmacro
     - (x &optional (y 'nil binary-casep))
     (if binary-casep
         (let ((y (if (and (consp y)
                           (eq (car y) 'quote)
                           (consp (cdr y))
                           (acl2-numberp (car (cdr y)))
                           (eq (cdr (cdr y)) nil))
                      (car (cdr y))
                      y)))
              (if (acl2-numberp y)
                  (cons 'binary-+
                        (cons (unary-- y) (cons x nil)))
                  (cons 'binary-+
                        (cons x
                              (cons (cons 'unary-- (cons y nil))
                                    nil)))))
         (let ((x (if (and (consp x)
                           (eq (car x) 'quote)
                           (consp (cdr x))
                           (acl2-numberp (car (cdr x)))
                           (eq (cdr (cdr x)) nil))
                      (car (cdr x))
                      x)))
              (if (acl2-numberp x)
                  (unary-- x)
                  (cons 'unary-- (cons x nil))))))