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

We introduce the function o-finp which returns t for any ordinal that is finite, else nil. This function is equivalent to the function atom, and is introduced so that we can disable its definition when dealing with ordinals (also see make-ord).

To see the ACL2 definition of this function, see pf.