		Search-engine friendly clone of the ACL2 documentation.

Constants-conversions-and-bounds

N80-to-i80

Signature
(n80-to-i80 x) → *
Arguments: x — Guard (n80p x).

Definitions and Theorems

Function: n80-to-i80$inline

(defun n80-to-i80$inline (x)
  (declare (type (unsigned-byte 80) x))
  (declare (xargs :guard (n80p x)))
  (mbe :logic (logext 80 x)
       :exec
       (if (< x 604462909807314587353088)
           x
         (- x 1208925819614629174706176))))