I24-to-n24
- Signature
(i24-to-n24 x) → *
- Arguments
- x — Guard (i24p x).
Definitions and Theorems
Function: i24-to-n24$inline
(defun i24-to-n24$inline (x)
(declare (type (signed-byte 24) x))
(declare (xargs :guard (i24p x)))
(mbe :logic (loghead 24 x)
:exec (if (>= x 0) x (+ x 16777216))))
