		Search-engine friendly clone of the ACL2 documentation.

O-rst

Returns the rest of an infinite ordinal

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.

Function: o-rst

(defun o-rst (x)
  (declare (xargs :guard (consp x)))
  (cdr x))