• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
      • Std/lists
      • Omaps
      • Std/alists
      • Obags
      • Std/util
      • Std/strings
      • Std/osets
      • Std/io
      • Std/basic
        • Maybe-stringp
        • Maybe-natp
        • Two-nats-measure
        • Impossible
        • Bytep
          • Byte
            • Byte-list
              • Byte-listp
                • Byte-listp-basics
              • Byte-list-fix
              • Byte-list20
              • Byte-list32
              • Byte-list64
              • Byte-list-equiv
            • Byte-fix
            • Bytep-additional-theorems
          • Bytes-as-digits-in-base-256
          • Bytep-additional-theorems
        • Nat-list-measure
        • Maybe-posp
        • Nibblep
        • Organize-symbols-by-pkg
        • Organize-symbols-by-name
        • Lnfix
        • Good-valuep
        • Streqv
        • Chareqv
        • Symbol-package-name-non-cl
        • Arith-equivs
        • Induction-schemes
        • Maybe-integerp
        • Char-fix
        • Pos-fix
        • Symbol-package-name-lst
        • Mbt$
        • Maybe-bitp
        • Good-pseudo-termp
        • Str-fix
        • Maybe-string-fix
        • Nonkeyword-listp
        • Lifix
        • Bfix
        • Std/basic/if*
        • Impliez
        • Tuplep
        • Std/basic/intern-in-package-of-symbol
        • Lbfix
        • Std/basic/symbol-name-lst
        • True
        • Std/basic/rfix
        • Std/basic/realfix
        • Std/basic/member-symbol-name
        • Std/basic/fix
        • False
        • Std/basic/nfix
        • Std/basic/ifix
      • Std/system
      • Std/typed-lists
      • Std/bitsets
      • Std/testing
      • Std/typed-alists
      • Std/stobjs
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Byte-list

Byte-listp

(byte-listp x) recognizes lists where every element satisfies bytep.

Signature
(byte-listp x) → *

This is an ordinary std::deflist. It is "strict" in that it requires x to be a "properly" nil-terminated list.

Subtopics

Byte-listp-basics
Basic theorems about byte-listp, generated by std::deflist.