N05-to-i05
- Signature
(n05-to-i05 x) → *
- Arguments
- x — Guard (n05p x).
Definitions and Theorems
Function: n05-to-i05$inline
(defun n05-to-i05$inline (x)
(declare (type (unsigned-byte 5) x))
(declare (xargs :guard (n05p x)))
(mbe :logic (logext 5 x)
:exec (if (< x 16) x (- x 32))))
