I45-to-n45
- Signature
(i45-to-n45 x) → *
- Arguments
- x — Guard (i45p x).
Definitions and Theorems
Function: i45-to-n45$inline
(defun i45-to-n45$inline (x)
(declare (type (signed-byte 45) x))
(declare (xargs :guard (i45p x)))
(mbe :logic (loghead 45 x)
:exec (if (>= x 0) x (+ x 35184372088832))))
