N17-to-i17
- Signature
(n17-to-i17 x) → *
- Arguments
- x — Guard (n17p x).
Definitions and Theorems
Function: n17-to-i17$inline
(defun n17-to-i17$inline (x)
(declare (type (unsigned-byte 17) x))
(declare (xargs :guard (n17p x)))
(mbe :logic (logext 17 x)
:exec (if (< x 65536) x (- x 131072))))