The first exponent of an ordinal
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 car of the first
pair in the list. In the case of a natural number, the value returned is
0 (since a natural number,
For the corresponding coefficient, see o-first-coeff.
(defun o-first-expt (x) (declare (xargs :guard (or (o-finp x) (consp (car x))))) (if (o-finp x) 0 (caar x)))