Major Section: ACL2-BUILT-INS
Realfix simply returns any real number argument unchanged,
0 on a non-real argument. Also see nfix,
see ifix, see rfix, and see fix for analogous functions
that coerce to a natural number, an integer, a rational, and a
Realfix has a guard of
To see the ACL2 definition of this function, see pf.