I18-to-n18
- Signature
(i18-to-n18 x) → *
- Arguments
- x — Guard (i18p x).
Definitions and Theorems
Function: i18-to-n18$inline
(defun i18-to-n18$inline (x)
(declare (type (signed-byte 18) x))
(declare (xargs :guard (i18p x)))
(mbe :logic (loghead 18 x)
:exec (if (>= x 0) x (+ x 262144))))
