		Search-engine friendly clone of the ACL2 documentation.

Jenkins-hash

U32-ash

Signature
(u32-ash i c) → shift
Returns: shift — Type (unsigned-byte-p 32 shift).

Definitions and Theorems

Function: u32-ash$inline

(defun u32-ash$inline (i c)
  (declare (type (unsigned-byte 32) i)
           (type (integer -31 31) c)
           (xargs :type-prescription (natp (u32-ash i c)))
           (optimize (speed 3) (safety 0)))
  (declare (xargs :guard t))
  (the (unsigned-byte 32)
       (logand (ash i c) *u32-max*)))

Theorem: return-type-of-u32-ash

(defthm return-type-of-u32-ash
  (b* ((shift (u32-ash$inline i c)))
    (unsigned-byte-p 32 shift))
  :rule-classes :rewrite)