		Search-engine friendly clone of the ACL2 documentation.

Constants-conversions-and-bounds

I120-to-n120

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

Definitions and Theorems

Function: i120-to-n120$inline

(defun i120-to-n120$inline (x)
  (declare (type (signed-byte 120) x))
  (declare (xargs :guard (i120p x)))
  (mbe :logic (loghead 120 x)
       :exec
       (if (>= x 0)
           x
         (+ x
            1329227995784915872903807060280344576))))