Major Section: ACL2-BUILT-INS
Zpf
is exactly the same as zp
, except that zpf
is intended for,
and faster for, fixnum arguments. Its guard is specified with a type
declaration, (type (unsigned-byte 29) x)
. (See declare and
see type-spec.) Also see zp.
To see the ACL2 definition of this function, see pf.