Major Section: ACL2-BUILT-INS
Make-ord is the ordinal constructor. Its use is recommended instead of
cons to make ordinals. For a discussion of ordinals,
For any ordinal,
alpha < epsilon-0, there exist natural numbers
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
x1 the ``first coefficient'', and the remainder
(w^(a2)x2 + ... + w^(an)xn + p) the ``rest'' of alpha.
(Make-ord fe fco rst) corresponds to the ordinal
(w^fe)fco + rst. Thus the first infinite ordinal,
(make-ord 1 1 0)and, for example, the ordinal
(w^2)5 + w2 + 7is constructed by:
(make-ord 2 5 (make-ord 1 2 7)) .
make-ord is used rather than
cons is that it
allows us to reason more abstractly about the ordinals, without
having to worry about the underlying representation.
To see the ACL2 definition of this function, see pf.