N25-to-i25
- Signature
(n25-to-i25 x) → *
- Arguments
- x — Guard (n25p x).
Definitions and Theorems
Function: n25-to-i25$inline
(defun n25-to-i25$inline (x)
(declare (type (unsigned-byte 25) x))
(declare (xargs :guard (n25p x)))
(mbe :logic (logext 25 x)
:exec (if (< x 16777216) x (- x 33554432))))
