I12-to-n12
- Signature
(i12-to-n12 x) → *
- Arguments
- x — Guard (i12p x).
Definitions and Theorems
Function: i12-to-n12$inline
(defun i12-to-n12$inline (x)
(declare (type (signed-byte 12) x))
(declare (xargs :guard (i12p x)))
(mbe :logic (loghead 12 x)
:exec (if (>= x 0) x (+ x 4096))))
