I33-to-n33
- Signature
(i33-to-n33 x) → *
- Arguments
- x — Guard (i33p x).
Definitions and Theorems
Function: i33-to-n33$inline
(defun i33-to-n33$inline (x)
(declare (type (signed-byte 33) x))
(declare (xargs :guard (i33p x)))
(mbe :logic (loghead 33 x)
:exec (if (>= x 0) x (+ x 8589934592))))
