I02-to-n02
- Signature
(i02-to-n02 x) → *
- Arguments
- x — Guard (i02p x).
Definitions and Theorems
Function: i02-to-n02$inline
(defun i02-to-n02$inline (x)
(declare (type (signed-byte 2) x))
(declare (xargs :guard (i02p x)))
(mbe :logic (loghead 2 x)
:exec (if (>= x 0) x (+ x 4))))
