		Search-engine friendly clone of the ACL2 documentation.

Binary--

Binary-minus-for-gl

Hack for implementing binary--. Don't use this.

Signature
(binary-minus-for-gl x y) → *
Arguments: x — Guard (acl2-numberp x).; y — Guard (acl2-numberp y).

You should never need to use this, call binary-- instead.

This is the logical definition for binary--. It has a custom GL symbolic counterpart. The only reason to make this a separate function, instead of directly putting a symbolic counterpart on binary-- itself, is to avoid infinite inlining problems when we define custom symbolic counterparts for inlined functions on Lisps like SBCL.

Definitions and Theorems

Function: binary-minus-for-gl

(defun binary-minus-for-gl (x y)
  (declare (xargs :guard (and (acl2-numberp x)
                              (acl2-numberp y))))
  (let ((__function__ 'binary-minus-for-gl))
    (declare (ignorable __function__))
    (- x y)))