N16-to-i16
- Signature
(n16-to-i16 x) → *
- Arguments
- x — Guard (n16p x).
Definitions and Theorems
Function: n16-to-i16$inline
(defun n16-to-i16$inline (x)
(declare (type (unsigned-byte 16) x))
(declare (xargs :guard (n16p x)))
(mbe :logic (logext 16 x)
:exec (if (< x 32768) x (- x 65536))))
