I48-to-n48
- Signature
(i48-to-n48 x) → *
- Arguments
- x — Guard (i48p x).
Definitions and Theorems
Function: i48-to-n48$inline
(defun i48-to-n48$inline (x)
(declare (type (signed-byte 48) x))
(declare (xargs :guard (i48p x)))
(mbe :logic (loghead 48 x)
:exec (if (>= x 0) x (+ x 281474976710656))))
