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