N09-to-i09
- Signature
(n09-to-i09 x) → *
- Arguments
- x — Guard (n09p x).
Definitions and Theorems
Function: n09-to-i09$inline
(defun n09-to-i09$inline (x)
(declare (type (unsigned-byte 9) x))
(declare (xargs :guard (n09p x)))
(mbe :logic (logext 9 x)
:exec (if (< x 256) x (- x 512))))
