N06-to-i06
- Signature
(n06-to-i06 x) → *
- Arguments
- x — Guard (n06p x).
Definitions and Theorems
Function: n06-to-i06$inline
(defun n06-to-i06$inline (x)
(declare (type (unsigned-byte 6) x))
(declare (xargs :guard (n06p x)))
(mbe :logic (logext 6 x)
:exec (if (< x 32) x (- x 64))))
