		Search-engine friendly clone of the ACL2 documentation.

Unsigned-saturate

Unsigned-saturate64

Optimized implementation of 64-bit unsigned saturation.

Signature
(unsigned-saturate64 x) → *
Arguments: x — Guard (integerp x).

Definitions and Theorems

Function: unsigned-saturate64$inline

(defun unsigned-saturate64$inline (x)
  (declare (xargs :guard (integerp x)))
  (let ((__function__ 'unsigned-saturate64))
    (declare (ignorable __function__))
    (mbe :logic (unsigned-saturate-fn 64 x)
         :exec (cond ((>= x 18446744073709551615)
                      18446744073709551615)
                     ((<= x 0) 0)
                     (t x)))))