		Search-engine friendly clone of the ACL2 documentation.

Constants-conversions-and-bounds

N128-to-i128

Signature
(n128-to-i128 x) → *
Arguments: x — Guard (n128p x).

Definitions and Theorems

Function: n128-to-i128$inline

(defun n128-to-i128$inline (x)
  (declare (type (unsigned-byte 128) x))
  (declare (xargs :guard (n128p x)))
  (mbe :logic (logext 128 x)
       :exec
       (if (< x
              170141183460469231731687303715884105728)
           x
         (- x
            340282366920938463463374607431768211456))))