N02-to-i02
- Signature
(n02-to-i02 x) → *
- Arguments
- x — Guard (n02p x).
Definitions and Theorems
Function: n02-to-i02$inline
(defun n02-to-i02$inline (x)
(declare (type (unsigned-byte 2) x))
(declare (xargs :guard (n02p x)))
(mbe :logic (logext 2 x)
:exec (if (< x 2) x (- x 4))))
