		Search-engine friendly clone of the ACL2 documentation.

Constants-conversions-and-bounds

N112-to-i112

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

Definitions and Theorems

Function: n112-to-i112$inline

(defun n112-to-i112$inline (x)
  (declare (type (unsigned-byte 112) x))
  (declare (xargs :guard (n112p x)))
  (mbe :logic (logext 112 x)
       :exec
       (if (< x 2596148429267413814265248164610048)
           x
         (- x 5192296858534827628530496329220096))))