N35-to-i35
- Signature
(n35-to-i35 x) → *
- Arguments
- x — Guard (n35p x).
Definitions and Theorems
Function: n35-to-i35$inline
(defun n35-to-i35$inline (x)
(declare (type (unsigned-byte 35) x))
(declare (xargs :guard (n35p x)))
(mbe :logic (logext 35 x)
:exec
(if (< x 17179869184)
x
(- x 34359738368))))
