(n01 x) → *
Function: n01$inline
(defun n01$inline (x) (declare (xargs :guard (integerp x))) (mbe :logic (loghead 1 x) :exec (logand 1 x)))