O-INFP

recognizes if an ordinal is infinite 
Major Section:  ACL2-BUILT-INS

O-infp is a macro. (O-infp x) opens up to (not (o-finp x)) (see o-finp).