I44-to-n44
- Signature
(i44-to-n44 x) → *
- Arguments
- x — Guard (i44p x).
Definitions and Theorems
Function: i44-to-n44$inline
(defun i44-to-n44$inline (x)
(declare (type (signed-byte 44) x))
(declare (xargs :guard (i44p x)))
(mbe :logic (loghead 44 x)
:exec (if (>= x 0) x (+ x 17592186044416))))
