O-RST

returns the rest of an infinite ordinal
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.