I30-to-n30
- Signature
(i30-to-n30 x) → *
- Arguments
- x — Guard (i30p x).
Definitions and Theorems
Function: i30-to-n30$inline
(defun i30-to-n30$inline (x)
(declare (type (signed-byte 30) x))
(declare (xargs :guard (i30p x)))
(mbe :logic (loghead 30 x)
:exec (if (>= x 0) x (+ x 1073741824))))
