I21-to-n21
- Signature
(i21-to-n21 x) → *
- Arguments
- x — Guard (i21p x).
Definitions and Theorems
Function: i21-to-n21$inline
(defun i21-to-n21$inline (x)
(declare (type (signed-byte 21) x))
(declare (xargs :guard (i21p x)))
(mbe :logic (loghead 21 x)
:exec (if (>= x 0) x (+ x 2097152))))
