		Search-engine friendly clone of the ACL2 documentation.

Constants-conversions-and-bounds

N55-to-i55

Signature
(n55-to-i55 x) → *
Arguments: x — Guard (n55p x).

Definitions and Theorems

Function: n55-to-i55$inline

(defun n55-to-i55$inline (x)
  (declare (type (unsigned-byte 55) x))
  (declare (xargs :guard (n55p x)))
  (mbe :logic (logext 55 x)
       :exec
       (if (< x 18014398509481984)
           x
         (- x 36028797018963968))))