ZPF

testing a nonnegative fixnum against 0
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.