I11-to-n11
- Signature
(i11-to-n11 x) → *
- Arguments
- x — Guard (i11p x).
Definitions and Theorems
Function: i11-to-n11$inline
(defun i11-to-n11$inline (x)
(declare (type (signed-byte 11) x))
(declare (xargs :guard (i11p x)))
(mbe :logic (loghead 11 x)
:exec (if (>= x 0) x (+ x 2048))))
