I17-to-n17
- Signature
(i17-to-n17 x) → *
- Arguments
- x — Guard (i17p x).
Definitions and Theorems
Function: i17-to-n17$inline
(defun i17-to-n17$inline (x)
(declare (type (signed-byte 17) x))
(declare (xargs :guard (i17p x)))
(mbe :logic (loghead 17 x)
:exec (if (>= x 0) x (+ x 131072))))
