I06-to-n06
- Signature
(i06-to-n06 x) → *
- Arguments
- x — Guard (i06p x).
Definitions and Theorems
Function: i06-to-n06$inline
(defun i06-to-n06$inline (x)
(declare (type (signed-byte 6) x))
(declare (xargs :guard (i06p x)))
(mbe :logic (loghead 6 x)
:exec (if (>= x 0) x (+ x 64))))
