I05-to-n05
- Signature
(i05-to-n05 x) → *
- Arguments
- x — Guard (i05p x).
Definitions and Theorems
Function: i05-to-n05$inline
(defun i05-to-n05$inline (x)
(declare (type (signed-byte 5) x))
(declare (xargs :guard (i05p x)))
(mbe :logic (loghead 5 x)
:exec (if (>= x 0) x (+ x 32))))
