IFIX

coerce to an integer
Major Section:  ACL2-BUILT-INS

Ifix simply returns any integer argument unchanged, returning 0 on a non-integer argument. Also see nfix, see rfix, see realfix and see fix for analogous functions that coerce to a natural number, a rational number, a real, and a number, respectively.

Ifix has a guard of t.

To see the ACL2 definition of this function, see pf.