		Search-engine friendly clone of the ACL2 documentation.

Constants-conversions-and-bounds

N65-to-i65

Signature
(n65-to-i65 x) → *
Arguments: x — Guard (n65p x).

Definitions and Theorems

Function: n65-to-i65$inline

(defun n65-to-i65$inline (x)
  (declare (type (unsigned-byte 65) x))
  (declare (xargs :guard (n65p x)))
  (mbe :logic (logext 65 x)
       :exec
       (if (< x 18446744073709551616)
           x
         (- x 36893488147419103232))))