N08-to-i08
- Signature
(n08-to-i08 x) → *
- Arguments
- x — Guard (n08p x).
Definitions and Theorems
Function: n08-to-i08$inline
(defun n08-to-i08$inline (x)
(declare (type (unsigned-byte 8) x))
(declare (xargs :guard (n08p x)))
(mbe :logic (logext 8 x)
:exec (if (< x 128) x (- x 256))))
