I47-to-n47
- Signature
(i47-to-n47 x) → *
- Arguments
- x — Guard (i47p x).
Definitions and Theorems
Function: i47-to-n47$inline
(defun i47-to-n47$inline (x)
(declare (type (signed-byte 47) x))
(declare (xargs :guard (i47p x)))
(mbe :logic (loghead 47 x)
:exec (if (>= x 0) x (+ x 140737488355328))))
