N11-to-i11
- Signature
(n11-to-i11 x) → *
- Arguments
- x — Guard (n11p x).
Definitions and Theorems
Function: n11-to-i11$inline
(defun n11-to-i11$inline (x)
(declare (type (unsigned-byte 11) x))
(declare (xargs :guard (n11p x)))
(mbe :logic (logext 11 x)
:exec (if (< x 1024) x (- x 2048))))
