I27-to-n27
- Signature
(i27-to-n27 x) → *
- Arguments
- x — Guard (i27p x).
Definitions and Theorems
Function: i27-to-n27$inline
(defun i27-to-n27$inline (x)
(declare (type (signed-byte 27) x))
(declare (xargs :guard (i27p x)))
(mbe :logic (loghead 27 x)
:exec (if (>= x 0) x (+ x 134217728))))
