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.