N18-to-i18
- Signature
(n18-to-i18 x) → *
- Arguments
- x — Guard (n18p x).
Definitions and Theorems
Function: n18-to-i18$inline
(defun n18-to-i18$inline (x)
(declare (type (unsigned-byte 18) x))
(declare (xargs :guard (n18p x)))
(mbe :logic (logext 18 x)
:exec (if (< x 131072) x (- x 262144))))
