N32-to-i32
- Signature
(n32-to-i32 x) → *
- Arguments
- x — Guard (n32p x).
Definitions and Theorems
Function: n32-to-i32$inline
(defun n32-to-i32$inline (x)
(declare (type (unsigned-byte 32) x))
(declare (xargs :guard (n32p x)))
(mbe :logic (logext 32 x)
:exec
(if (< x 2147483648)
x
(- x 4294967296))))
