I65-to-n65
- Signature
(i65-to-n65 x) → *
- Arguments
- x — Guard (i65p x).
Definitions and Theorems
Function: i65-to-n65$inline
(defun i65-to-n65$inline (x)
(declare (type (signed-byte 65) x))
(declare (xargs :guard (i65p x)))
(mbe :logic (loghead 65 x)
:exec
(if (>= x 0)
x
(+ x 36893488147419103232))))
