I60-to-n60
- Signature
(i60-to-n60 x) → *
- Arguments
- x — Guard (i60p x).
Definitions and Theorems
Function: i60-to-n60$inline
(defun i60-to-n60$inline (x)
(declare (type (signed-byte 60) x))
(declare (xargs :guard (i60p x)))
(mbe :logic (loghead 60 x)
:exec
(if (>= x 0)
x
(+ x 1152921504606846976))))
