I32-to-n32
- Signature
(i32-to-n32 x) → *
- Arguments
- x — Guard (i32p x).
Definitions and Theorems
Function: i32-to-n32$inline
(defun i32-to-n32$inline (x)
(declare (type (signed-byte 32) x))
(declare (xargs :guard (i32p x)))
(mbe :logic (loghead 32 x)
:exec (if (>= x 0) x (+ x 4294967296))))
