## E0-ORDINALP

the old recognizer for ACL2 ordinals
Major Section: PROGRAMMING

See o-p for the current recognizer for ACL2 ordinals.

The functions `e0-ordinalp`

and `e0-ord-<`

were replaced in ACL2
Version_2.8 by `o-p`

and `o<`

, respectively. However, books created
before that version used the earlier functions for termination proofs; the
old functions might be of use in these cases. To use the old functions in
termination proofs, include the book `books/ordinals/e0-ordinal`

and
execute the event `(set-well-founded-relation e0-ord-<)`

(see set-well-founded-relation). For a more thorough discussion of
these functions, see the documentation at the end of
`books/ordinals/e0-ordinal.lisp`

.