• 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
        • Defun
        • Declare
        • System-utilities
        • Stobj
        • State
        • Mutual-recursion
        • Memoize
        • Mbe
        • Io
        • Defpkg
        • Apply$
        • Loop$
        • Programming-with-state
        • Arrays
        • Characters
        • Time$
        • Defmacro
        • Loop$-primer
        • Fast-alists
        • Defconst
        • Evaluation
        • Guard
        • Equality-variants
        • Compilation
        • Hons
        • ACL2-built-ins
        • Developers-guide
        • System-attachments
        • Advanced-features
        • Set-check-invariant-risk
        • Numbers
        • Efficiency
        • Irrelevant-formals
        • Introduction-to-programming-in-ACL2-for-those-who-know-lisp
        • Redefining-programs
        • Lists
        • Invariant-risk
        • Errors
        • Defabbrev
        • Conses
        • Alists
        • Set-register-invariant-risk
        • Strings
        • Program-wrapper
        • Get-internal-time
        • Basics
          • Let
          • Return-last
          • Mv-let
          • Flet
          • Or
          • Mv
          • And
          • Booleanp
          • If
          • Not
          • Equal
            • Eql
            • Eq
            • =
            • Eqlablep
              • Eqlable-listp
            • Hons-equal
            • Eqlable-listp
          • Implies
          • Iff
          • Macrolet
          • Quote
          • Let*
          • Case-match
          • ACL2-count
          • Case
          • Good-bye
          • Cond
          • Null
          • Progn$
          • Identity
          • Xor
        • Packages
        • Oracle-eval
        • Defmacro-untouchable
        • <<
        • Primitive
        • Revert-world
        • Unmemoize
        • Set-duplicate-keys-action
        • Symbols
        • Def-list-constructor
        • Easy-simplify-term
        • Defiteration
        • Fake-oracle-eval
        • Defopen
        • Sleep
      • Operational-semantics
      • Real
      • Start-here
      • Debugging
      • Miscellaneous
      • Output-controls
      • Macros
      • Interfacing-tools
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Equal
  • ACL2-built-ins

Eqlablep

The guard for the function eql

The predicate eqlablep tests whether its argument is suitable for eql, at least one of whose arguments must satisfy this predicate in Common Lisp. (Eqlablep x) is true if and only if its argument is a number, a symbol, or a character.

Function: eqlablep

(defun eqlablep (x)
  (declare (xargs :guard t))
  (or (acl2-numberp x)
      (symbolp x)
      (characterp x)))

Subtopics

Eqlable-listp
Recognizer for a true list of objects each suitable for eql