		Search-engine friendly clone of the ACL2 documentation.

Constants-conversions-and-bounds

N45-to-i45

Signature
(n45-to-i45 x) → *
Arguments: x — Guard (n45p x).

Definitions and Theorems

Function: n45-to-i45$inline

(defun n45-to-i45$inline (x)
  (declare (type (unsigned-byte 45) x))
  (declare (xargs :guard (n45p x)))
  (mbe :logic (logext 45 x)
       :exec
       (if (< x 17592186044416)
           x
         (- x 35184372088832))))