		Search-engine friendly clone of the ACL2 documentation.

I44

Function: i44$inline

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