I26-to-n26
- Signature
(i26-to-n26 x) → *
- Arguments
- x — Guard (i26p x).
Definitions and Theorems
Function: i26-to-n26$inline
(defun i26-to-n26$inline (x)
(declare (type (signed-byte 26) x))
(declare (xargs :guard (i26p x)))
(mbe :logic (loghead 26 x)
:exec (if (>= x 0) x (+ x 67108864))))
