N22-to-i22
- Signature
(n22-to-i22 x) → *
- Arguments
- x — Guard (n22p x).
Definitions and Theorems
Function: n22-to-i22$inline
(defun n22-to-i22$inline (x)
(declare (type (unsigned-byte 22) x))
(declare (xargs :guard (n22p x)))
(mbe :logic (logext 22 x)
:exec (if (< x 2097152) x (- x 4194304))))
