		Search-engine friendly clone of the ACL2 documentation.

Constants-conversions-and-bounds

N120-to-i120

Signature
(n120-to-i120 x) → *
Arguments: x — Guard (n120p x).

Definitions and Theorems

Function: n120-to-i120$inline

(defun n120-to-i120$inline (x)
  (declare (type (unsigned-byte 120) x))
  (declare (xargs :guard (n120p x)))
  (mbe :logic (logext 120 x)
       :exec
       (if (< x 664613997892457936451903530140172288)
           x
         (- x
            1329227995784915872903807060280344576))))