		Search-engine friendly clone of the ACL2 documentation.

Constants-conversions-and-bounds

I512-to-n512

Signature
(i512-to-n512 x) → *
Arguments: x — Guard (i512p x).

Definitions and Theorems

Function: i512-to-n512$inline

(defun i512-to-n512$inline (x)
 (declare (type (signed-byte 512) x))
 (declare (xargs :guard (i512p x)))
 (mbe
  :logic (loghead 512 x)
  :exec
  (if (>= x 0)
      x
   (+
    x
    13407807929942597099574024998205846127479365820592393377723561443721764030073546976801874298166903427690031858186486050853753882811946569946433649006084096))))