I59-to-n59
- Signature
(i59-to-n59 x) → *
- Arguments
- x — Guard (i59p x).
Definitions and Theorems
Function: i59-to-n59$inline
(defun i59-to-n59$inline (x)
(declare (type (signed-byte 59) x))
(declare (xargs :guard (i59p x)))
(mbe :logic (loghead 59 x)
:exec
(if (>= x 0)
x
(+ x 576460752303423488))))
