I03-to-n03
- Signature
(i03-to-n03 x) → *
- Arguments
- x — Guard (i03p x).
Definitions and Theorems
Function: i03-to-n03$inline
(defun i03-to-n03$inline (x)
(declare (type (signed-byte 3) x))
(declare (xargs :guard (i03p x)))
(mbe :logic (loghead 3 x)
:exec (if (>= x 0) x (+ x 8))))
