I52-to-n52
- Signature
(i52-to-n52 x) → *
- Arguments
- x — Guard (i52p x).
Definitions and Theorems
Function: i52-to-n52$inline
(defun i52-to-n52$inline (x)
(declare (type (signed-byte 52) x))
(declare (xargs :guard (i52p x)))
(mbe :logic (loghead 52 x)
:exec (if (>= x 0) x (+ x 4503599627370496))))
