Major Section: ACL2-BUILT-INS
An ACL2 ordinal is either a natural number or, for an infinite ordinal, a
list whose elements are exponent-coefficient pairs (see o-p). In the latter
case, this function returns the cdr of the first pair in the list. In
the case of a natural number, this function returns the ordinal itself
(since a natural number, n, can be thought of as (w^0)n).
For the corresponding exponent, see o-first-expt.
To see the ACL2 definition of this function, see pf.
