N04-to-i04
- Signature
(n04-to-i04 x) → *
- Arguments
- x — Guard (n04p x).
Definitions and Theorems
Function: n04-to-i04$inline
(defun n04-to-i04$inline (x)
(declare (type (unsigned-byte 4) x))
(declare (xargs :guard (n04p x)))
(mbe :logic (logext 4 x)
:exec (if (< x 8) x (- x 16))))
