N12-to-i12
- Signature
(n12-to-i12 x) → *
- Arguments
- x — Guard (n12p x).
Definitions and Theorems
Function: n12-to-i12$inline
(defun n12-to-i12$inline (x)
(declare (type (unsigned-byte 12) x))
(declare (xargs :guard (n12p x)))
(mbe :logic (logext 12 x)
:exec (if (< x 2048) x (- x 4096))))
