		Search-engine friendly clone of the ACL2 documentation.

Constants-conversions-and-bounds

N43-to-i43

Signature
(n43-to-i43 x) → *
Arguments: x — Guard (n43p x).

Definitions and Theorems

Function: n43-to-i43$inline

(defun n43-to-i43$inline (x)
  (declare (type (unsigned-byte 43) x))
  (declare (xargs :guard (n43p x)))
  (mbe :logic (logext 43 x)
       :exec
       (if (< x 4398046511104)
           x
         (- x 8796093022208))))