I01-to-n01
- Signature
(i01-to-n01 x) → *
- Arguments
- x — Guard (i01p x).
Definitions and Theorems
Function: i01-to-n01$inline
(defun i01-to-n01$inline (x)
(declare (type (signed-byte 1) x))
(declare (xargs :guard (i01p x)))
(mbe :logic (loghead 1 x)
:exec (if (>= x 0) x (+ x 2))))
