N30-to-i30
- Signature
(n30-to-i30 x) → *
- Arguments
- x — Guard (n30p x).
Definitions and Theorems
Function: n30-to-i30$inline
(defun n30-to-i30$inline (x)
(declare (type (unsigned-byte 30) x))
(declare (xargs :guard (n30p x)))
(mbe :logic (logext 30 x)
:exec
(if (< x 536870912)
x
(- x 1073741824))))
