N26-to-i26
- Signature
(n26-to-i26 x) → *
- Arguments
- x — Guard (n26p x).
Definitions and Theorems
Function: n26-to-i26$inline
(defun n26-to-i26$inline (x)
(declare (type (unsigned-byte 26) x))
(declare (xargs :guard (n26p x)))
(mbe :logic (logext 26 x)
:exec (if (< x 33554432) x (- x 67108864))))
