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