I09-to-n09
- Signature
(i09-to-n09 x) → *
- Arguments
- x — Guard (i09p x).
Definitions and Theorems
Function: i09-to-n09$inline
(defun i09-to-n09$inline (x)
(declare (type (signed-byte 9) x))
(declare (xargs :guard (i09p x)))
(mbe :logic (loghead 9 x)
:exec (if (>= x 0) x (+ x 512))))
