N27-to-i27
- Signature
(n27-to-i27 x) → *
- Arguments
- x — Guard (n27p x).
Definitions and Theorems
Function: n27-to-i27$inline
(defun n27-to-i27$inline (x)
(declare (type (unsigned-byte 27) x))
(declare (xargs :guard (n27p x)))
(mbe :logic (logext 27 x)
:exec (if (< x 67108864) x (- x 134217728))))
