I16-to-n16
- Signature
(i16-to-n16 x) → *
- Arguments
- x — Guard (i16p x).
Definitions and Theorems
Function: i16-to-n16$inline
(defun i16-to-n16$inline (x)
(declare (type (signed-byte 16) x))
(declare (xargs :guard (i16p x)))
(mbe :logic (loghead 16 x)
:exec (if (>= x 0) x (+ x 65536))))
