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.
