		Search-engine friendly clone of the ACL2 documentation.

Symbolic-arithmetic

Int-set-sign

Change the sign bit of an integer to a new value.

Signature
(int-set-sign negp i) → new-i
Arguments: negp — True if we should set the sign bit to 1.; i — The integer to modify.
Guard (integerp i).
Returns: new-i — Type (integerp new-i).

Definitions and Theorems

Function: int-set-sign

(defun int-set-sign (negp i)
  (declare (xargs :guard (integerp i)))
  (let ((__function__ 'int-set-sign))
    (declare (ignorable __function__))
    (let ((i (lifix i)))
      (logapp (integer-length i)
              i (if negp -1 0)))))

Theorem: integerp-of-int-set-sign

(defthm integerp-of-int-set-sign
  (b* ((new-i (int-set-sign negp i)))
    (integerp new-i))
  :rule-classes :type-prescription)

Theorem: sign-of-int-set-sign

(defthm sign-of-int-set-sign
  (iff (< (int-set-sign negp i) 0) negp))