I64-to-n64
- Signature
(i64-to-n64 x) → *
- Arguments
- x — Guard (i64p x).
Definitions and Theorems
Function: i64-to-n64$inline
(defun i64-to-n64$inline (x)
(declare (type (signed-byte 64) x))
(declare (xargs :guard (i64p x)))
(mbe :logic (loghead 64 x)
:exec
(if (>= x 0)
x
(+ x 18446744073709551616))))