I35-to-n35
- Signature
(i35-to-n35 x) → *
- Arguments
- x — Guard (i35p x).
Definitions and Theorems
Function: i35-to-n35$inline
(defun i35-to-n35$inline (x)
(declare (type (signed-byte 35) x))
(declare (xargs :guard (i35p x)))
(mbe :logic (loghead 35 x)
:exec (if (>= x 0) x (+ x 34359738368))))
