I20-to-n20
- Signature
(i20-to-n20 x) → *
- Arguments
- x — Guard (i20p x).
Definitions and Theorems
Function: i20-to-n20$inline
(defun i20-to-n20$inline (x)
(declare (type (signed-byte 20) x))
(declare (xargs :guard (i20p x)))
(mbe :logic (loghead 20 x)
:exec (if (>= x 0) x (+ x 1048576))))
