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