Major Section: ACL2-BUILT-INS
Ifix simply returns any integer argument unchanged, returning
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,
Ifix has a guard of
To see the ACL2 definition of this function, see pf.