• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Recursion-and-induction
      • Hons-and-memoization
      • Events
      • Parallelism
      • History
      • Programming
      • Operational-semantics
      • Real
      • Start-here
      • Debugging
      • Miscellaneous
        • Term
        • Ld
        • Hints
        • Type-set
        • Ordinals
          • O-p
          • O<
          • Proof-of-well-foundedness
          • Two-nats-measure
          • Nat-list-measure
          • Make-ord
          • O-first-coeff
          • E0-ord-<
          • O-first-expt
          • E0-ordinalp
            • O-rst
            • O-finp
            • O>=
            • O<=
            • O-infp
            • O>
          • Clause
          • ACL2-customization
          • With-prover-step-limit
          • Set-prover-step-limit
          • With-prover-time-limit
          • Local-incompatibility
          • Set-case-split-limitations
          • Subversive-recursions
          • Specious-simplification
          • Defsum
          • Gcl
          • Oracle-timelimit
          • Thm
          • Defopener
          • Case-split-limitations
          • Set-gc-strategy
          • Default-defun-mode
          • Top-level
          • Reader
          • Ttags-seen
          • Adviser
          • Ttree
          • Abort-soft
          • Defsums
          • Gc$
          • With-timeout
          • Coi-debug::fail
          • Expander
          • Gc-strategy
          • Coi-debug::assert
          • Sin-cos
          • Def::doc
          • Syntax
          • Subversive-inductions
        • Output-controls
        • Macros
        • Interfacing-tools
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Ordinals

    E0-ordinalp

    The old recognizer for ACL2 ordinals.

    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, you can do:

    (include-book "ordinals/e0-ordinal" :dir :system)
(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 community book ordinals/e0-ordinal.lisp.