Major Section: ACL2-BUILT-INS
An ACL2 infinite ordinal is a list whose elements are exponent-coefficient
pairs (see o-p and see o-infp). The first exponent and first coefficient
of an ordinal can be obtained by using o-first-expt and
o-first-coeff respectively. To obtain the rest of the ordinal (for
recursive analysis), use the o-rst function. It returns the rest of the
ordinal after the first exponent and coefficient are removed.
To see the ACL2 definition of this function, see pf.
