|
|
|---|
|
|
|
|---|
Returns the first coefficient 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 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.
Function:
(defun o-first-coeff (x) (declare (xargs :guard (or (o-finp x) (consp (car x))))) (if (o-finp x) x (cdar x)))