N21-to-i21
- Signature
(n21-to-i21 x) → *
- Arguments
- x — Guard (n21p x).
Definitions and Theorems
Function: n21-to-i21$inline
(defun n21-to-i21$inline (x)
(declare (type (unsigned-byte 21) x))
(declare (xargs :guard (n21p x)))
(mbe :logic (logext 21 x)
:exec (if (< x 1048576) x (- x 2097152))))
