I55-to-n55
- Signature
(i55-to-n55 x) → *
- Arguments
- x — Guard (i55p x).
Definitions and Theorems
Function: i55-to-n55$inline
(defun i55-to-n55$inline (x)
(declare (type (signed-byte 55) x))
(declare (xargs :guard (i55p x)))
(mbe :logic (loghead 55 x)
:exec
(if (>= x 0)
x
(+ x 36028797018963968))))
