		Search-engine friendly clone of the ACL2 documentation.

Constants-conversions-and-bounds

N60-to-i60

Signature
(n60-to-i60 x) → *
Arguments: x — Guard (n60p x).

Definitions and Theorems

Function: n60-to-i60$inline

(defun n60-to-i60$inline (x)
  (declare (type (unsigned-byte 60) x))
  (declare (xargs :guard (n60p x)))
  (mbe :logic (logext 60 x)
       :exec
       (if (< x 576460752303423488)
           x
         (- x 1152921504606846976))))