### O-FINP

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.