		Search-engine friendly clone of the ACL2 documentation.

Lifix

(lifix x) is logically identical to (ifix x), but its guard requires that x is an integer and, in the execution, it is just a no-op that returns x.

(lifix x) is an inlined, enabled function that just expands into

(mbe :logic (ifix x) :exec x)

To understand why you might want this, see the analogous discussion about lnfix.

Function: lifix$inline

(defun lifix$inline (x)
  (declare (xargs :guard (integerp x)))
  (mbe :logic (ifix x) :exec x))