N20-to-i20
- Signature
(n20-to-i20 x) → *
- Arguments
- x — Guard (n20p x).
Definitions and Theorems
Function: n20-to-i20$inline
(defun n20-to-i20$inline (x)
(declare (type (unsigned-byte 20) x))
(declare (xargs :guard (n20p x)))
(mbe :logic (logext 20 x)
:exec (if (< x 524288) x (- x 1048576))))
