• 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
      • Std/system
      • Std/typed-lists
        • Std/typed-lists/character-listp
        • Std/typed-lists/symbol-listp
        • Std/typed-lists/boolean-listp
        • Std/typed-lists/string-listp
        • Std/typed-lists/eqlable-listp
        • Theorems-about-true-list-lists
        • Std/typed-lists/atom-listp
        • Unsigned-byte-listp
          • Defbytelist
            • Defbytelist-standard-instances
              • Ubyte8-list
              • Ubyte4-list
              • Ubyte32-list
              • Ubyte256-list
              • Ubyte128-list
              • Ubyte64-list
              • Ubyte3-list
              • Ubyte2-list
              • Ubyte16-list
              • Ubyte11-list
                • Ubyte11-list-fix
                • Ubyte11-list-equiv
                • Ubyte11-listp
                  • Ubyte11-listp-basics
              • Ubyte1-list
              • Sbyte8-list
              • Sbyte64-list
              • Sbyte4-list
              • Sbyte32-list
              • Sbyte3-list
              • Sbyte256-list
              • Sbyte2-list
              • Sbyte16-list
              • Sbyte128-list
              • Sbyte1-list
              • Defubytelist
              • Defsbytelist
            • Defbytelist-implementation
          • Unsigned-byte-list-fix
        • Cons-listp
        • Cons-list-listp
        • Signed-byte-listp
        • String-or-symbol-listp
      • Std/bitsets
      • Std/testing
      • Std/typed-alists
      • Std/stobjs
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Ubyte11-list

Ubyte11-listp

(ubyte11-listp x) recognizes lists where every element satisfies ubyte11p.

Signature
(ubyte11-listp x) → *

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

Subtopics

Ubyte11-listp-basics
Basic theorems about ubyte11-listp, generated by std::deflist.