N28-to-i28
- Signature
(n28-to-i28 x) → *
- Arguments
- x — Guard (n28p x).
Definitions and Theorems
Function: n28-to-i28$inline
(defun n28-to-i28$inline (x)
(declare (type (unsigned-byte 28) x))
(declare (xargs :guard (n28p x)))
(mbe :logic (logext 28 x)
:exec (if (< x 134217728) x (- x 268435456))))
