I43-to-n43
- Signature
(i43-to-n43 x) → *
- Arguments
- x — Guard (i43p x).
Definitions and Theorems
Function: i43-to-n43$inline
(defun i43-to-n43$inline (x)
(declare (type (signed-byte 43) x))
(declare (xargs :guard (i43p x)))
(mbe :logic (loghead 43 x)
:exec (if (>= x 0) x (+ x 8796093022208))))
