I25-to-n25
- Signature
(i25-to-n25 x) → *
- Arguments
- x — Guard (i25p x).
Definitions and Theorems
Function: i25-to-n25$inline
(defun i25-to-n25$inline (x)
(declare (type (signed-byte 25) x))
(declare (xargs :guard (i25p x)))
(mbe :logic (loghead 25 x)
:exec (if (>= x 0) x (+ x 33554432))))
