N03-to-i03
- Signature
(n03-to-i03 x) → *
- Arguments
- x — Guard (n03p x).
Definitions and Theorems
Function: n03-to-i03$inline
(defun n03-to-i03$inline (x)
(declare (type (unsigned-byte 3) x))
(declare (xargs :guard (n03p x)))
(mbe :logic (logext 3 x)
:exec (if (< x 4) x (- x 8))))
