N33-to-i33
- Signature
(n33-to-i33 x) → *
- Arguments
- x — Guard (n33p x).
Definitions and Theorems
Function: n33-to-i33$inline
(defun n33-to-i33$inline (x)
(declare (type (unsigned-byte 33) x))
(declare (xargs :guard (n33p x)))
(mbe :logic (logext 33 x)
:exec
(if (< x 4294967296)
x
(- x 8589934592))))
