I49-to-n49
- Signature
(i49-to-n49 x) → *
- Arguments
- x — Guard (i49p x).
Definitions and Theorems
Function: i49-to-n49$inline
(defun i49-to-n49$inline (x)
(declare (type (signed-byte 49) x))
(declare (xargs :guard (i49p x)))
(mbe :logic (loghead 49 x)
:exec (if (>= x 0) x (+ x 562949953421312))))
