		Search-engine friendly clone of the ACL2 documentation.

Constants-conversions-and-bounds

N52-to-i52

Signature
(n52-to-i52 x) → *
Arguments: x — Guard (n52p x).

Definitions and Theorems

Function: n52-to-i52$inline

(defun n52-to-i52$inline (x)
  (declare (type (unsigned-byte 52) x))
  (declare (xargs :guard (n52p x)))
  (mbe :logic (logext 52 x)
       :exec
       (if (< x 2251799813685248)
           x
         (- x 4503599627370496))))