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.
