		Search-engine friendly clone of the ACL2 documentation.

Constants-conversions-and-bounds

N47-to-i47

Signature
(n47-to-i47 x) → *
Arguments: x — Guard (n47p x).

Definitions and Theorems

Function: n47-to-i47$inline

(defun n47-to-i47$inline (x)
  (declare (type (unsigned-byte 47) x))
  (declare (xargs :guard (n47p x)))
  (mbe :logic (logext 47 x)
       :exec
       (if (< x 70368744177664)
           x
         (- x 140737488355328))))