• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Hons-and-memoization
      • Events
      • History
      • Parallelism
      • Programming
      • Start-here
      • Real
        • Standardp
        • Standard-part
        • I-limited
          • I-close
          • I-small
          • I-large
          • Real-listp
        • Debugging
        • Miscellaneous
        • Output-controls
        • Macros
        • Interfacing-tools
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • Real

    I-limited

    ACL2(r) recognizer for limited numbers

    (I-limited x) is true if and only if x is a number that is not infinitely large. This predicate is only defined in ACL2(r) (see real).