• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
      • Std/lists
      • Std/alists
      • Obags
      • Std/util
        • Defprojection
        • Deflist
        • Defaggregate
        • Define
        • Defmapping
        • Defenum
        • Add-io-pairs
        • Defalist
        • Defmapappend
        • Returns-specifiers
        • Defarbrec
        • Defines
        • Define-sk
        • Error-value-tuples
        • Defmax-nat
        • Defmin-int
        • Deftutorial
        • Extended-formals
        • Defrule
        • Defval
        • Defsurj
        • Defiso
        • Defconstrained-recognizer
        • Deffixer
        • Defmvtypes
        • Defconsts
        • Defthm-unsigned-byte-p
        • Support
          • Extract-keywords
          • Dumb-string-sublis
          • Raise
          • Look-up-return-vals
          • Logic-mode-p
          • Look-up-wrapper-args
          • Look-up-formals
          • Legal-kwds-p
          • Split-///
          • Keyword-legality
          • Getarg+
          • Var-is-stobj-p
          • Look-up-guard
          • Getarg
          • Cons-listp
            • Tuplep
            • Tuple-listp
            • Ends-with-period-p
          • Defthm-signed-byte-p
          • Defthm-natp
          • Defund-sk
          • Defmacro+
          • Defsum
          • Defthm-commutative
          • Definj
          • Defirrelevant
          • Defredundant
        • Std/strings
        • Std/osets
        • Std/io
        • Std/basic
        • Std/system
        • Std/typed-lists
        • Std/bitsets
        • Std/testing
        • Std/typed-alists
        • Std/stobjs
      • Community
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Support

    Cons-listp

    (cons-listp x) is like alistp but does not require the list to be nil-terminated.

    Definitions and Theorems

    Function: cons-listp

    (defun cons-listp (x)
      (declare (xargs :guard t))
      (if (consp x)
          (and (consp (car x))
               (cons-listp (cdr x)))
        t))