		Search-engine friendly clone of the ACL2 documentation.

I22

Function: i22$inline

(defun i22$inline (x)
  (declare (xargs :guard (integerp x)))
  (mbe :logic (logext 22 x)
       :exec (fast-logext 22 x)))