I28-to-n28
- Signature
(i28-to-n28 x) → *
- Arguments
- x — Guard (i28p x).
Definitions and Theorems
Function: i28-to-n28$inline
(defun i28-to-n28$inline (x)
(declare (type (signed-byte 28) x))
(declare (xargs :guard (i28p x)))
(mbe :logic (loghead 28 x)
:exec (if (>= x 0) x (+ x 268435456))))
