		Search-engine friendly clone of the ACL2 documentation.

Constants-conversions-and-bounds

N49-to-i49

Signature
(n49-to-i49 x) → *
Arguments: x — Guard (n49p x).

Definitions and Theorems

Function: n49-to-i49$inline

(defun n49-to-i49$inline (x)
  (declare (type (unsigned-byte 49) x))
  (declare (xargs :guard (n49p x)))
  (mbe :logic (logext 49 x)
       :exec
       (if (< x 281474976710656)
           x
         (- x 562949953421312))))