		Search-engine friendly clone of the ACL2 documentation.

Svmask-for-signx

Mask-for-fixed-signx

Signature
(mask-for-fixed-signx mask n) → mask
Arguments: mask — Guard (4vmask-p mask).; n — Guard (natp n).
Returns: mask — Type (4vmask-p mask).

Definitions and Theorems

Function: mask-for-fixed-signx$inline

(defun mask-for-fixed-signx$inline (mask n)
 (declare (xargs :guard (and (4vmask-p mask) (natp n))))
 (let ((__function__ 'mask-for-fixed-signx))
  (declare (ignorable __function__))
  (if (zp n)
      (if (sparseint-equal mask 0) 0 1)
   (sparseint-bitor
     (sparseint-concatenate n mask 0)
     (if (sparseint-test-bitand mask (sparseint-concatenate n 0 -1))
         (sparseint-concatenate (- n 1) 0 1)
       0)))))

Theorem: 4vmask-p-of-mask-for-fixed-signx

(defthm 4vmask-p-of-mask-for-fixed-signx
  (b* ((mask (mask-for-fixed-signx$inline mask n)))
    (4vmask-p mask))
  :rule-classes :rewrite)