N01-to-i01
- Signature
(n01-to-i01 x) → *
- Arguments
- x — Guard (n01p x).
Definitions and Theorems
Function: n01-to-i01$inline
(defun n01-to-i01$inline (x)
(declare (type (unsigned-byte 1) x))
(declare (xargs :guard (n01p x)))
(mbe :logic (logext 1 x)
:exec (if (< x 1) x (- x 2))))
