		Search-engine friendly clone of the ACL2 documentation.

O-first-expt

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, n, can be thought of as (w^0)n).

For the corresponding coefficient, see o-first-coeff.

Function: o-first-expt

(defun o-first-expt (x)
  (declare (xargs :guard (or (o-finp x) (consp (car x)))))
  (if (o-finp x) 0 (caar x)))