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.