a constructor for ordinals.
Major Section:  ACL2-BUILT-INS

Make-ord is the ordinal constructor. Its use is recommended instead of using cons to make ordinals. For a discussion of ordinals, see ordinals.

For any ordinal, alpha < epsilon-0, there exist natural numbers p and n, positive integers x1, x2, ..., xn and ordinals a1 > a2 > ... > an > 0 such that alpha > a1 and alpha = w^(a1)x1 + w^(a2)x2 + ... + w^(an)xn + p. We call a1 the ``first exponent'', x1 the ``first coefficient'', and the remainder (w^(a2)x2 + ... + w^(an)xn + p) the ``rest'' of alpha.


(make-ord 1 1 0)


To see the ACL2 definition of this function, see pf.