		Search-engine friendly clone of the ACL2 documentation.

Constants-conversions-and-bounds

I256-to-n256

Signature
(i256-to-n256 x) → *
Arguments: x — Guard (i256p x).

Definitions and Theorems

Function: i256-to-n256$inline

(defun i256-to-n256$inline (x)
 (declare (type (signed-byte 256) x))
 (declare (xargs :guard (i256p x)))
 (mbe
  :logic (loghead 256 x)
  :exec
  (if (>= x 0)
      x
   (+
    x
    115792089237316195423570985008687907853269984665640564039457584007913129639936))))