• 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
    • Lists
    • ACL2-built-ins

    Real-listp

    ACL2(r) recognizer for a true list of real numbers

    The predicate real-listp tests whether its argument is a true list of real numbers. This predicate is only defined in ACL2(r) (see real).