I22-to-n22
- Signature
(i22-to-n22 x) → *
- Arguments
- x — Guard (i22p x).
Definitions and Theorems
Function: i22-to-n22$inline
(defun i22-to-n22$inline (x)
(declare (type (signed-byte 22) x))
(declare (xargs :guard (i22p x)))
(mbe :logic (loghead 22 x)
:exec (if (>= x 0) x (+ x 4194304))))
