		Search-engine friendly clone of the ACL2 documentation.

Constants-conversions-and-bounds

I112-to-n112

Signature
(i112-to-n112 x) → *
Arguments: x — Guard (i112p x).

Definitions and Theorems

Function: i112-to-n112$inline

(defun i112-to-n112$inline (x)
  (declare (type (signed-byte 112) x))
  (declare (xargs :guard (i112p x)))
  (mbe :logic (loghead 112 x)
       :exec
       (if (>= x 0)
           x
         (+ x 5192296858534827628530496329220096))))