I04-to-n04
- Signature
(i04-to-n04 x) → *
- Arguments
- x — Guard (i04p x).
Definitions and Theorems
Function: i04-to-n04$inline
(defun i04-to-n04$inline (x)
(declare (type (signed-byte 4) x))
(declare (xargs :guard (i04p x)))
(mbe :logic (loghead 4 x)
:exec (if (>= x 0) x (+ x 16))))
