I51-to-n51
- Signature
(i51-to-n51 x) → *
- Arguments
- x — Guard (i51p x).
Definitions and Theorems
Function: i51-to-n51$inline
(defun i51-to-n51$inline (x)
(declare (type (signed-byte 51) x))
(declare (xargs :guard (i51p x)))
(mbe :logic (loghead 51 x)
:exec (if (>= x 0) x (+ x 2251799813685248))))
