I08-to-n08
- Signature
(i08-to-n08 x) → *
- Arguments
- x — Guard (i08p x).
Definitions and Theorems
Function: i08-to-n08$inline
(defun i08-to-n08$inline (x)
(declare (type (signed-byte 8) x))
(declare (xargs :guard (i08p x)))
(mbe :logic (loghead 8 x)
:exec (if (>= x 0) x (+ x 256))))
