N24-to-i24
- Signature
(n24-to-i24 x) → *
- Arguments
- x — Guard (n24p x).
Definitions and Theorems
Function: n24-to-i24$inline
(defun n24-to-i24$inline (x)
(declare (type (unsigned-byte 24) x))
(declare (xargs :guard (n24p x)))
(mbe :logic (logext 24 x)
:exec (if (< x 8388608) x (- x 16777216))))
