• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Error-checking
        • Apt
        • Abnf
        • Fty-extensions
          • Defbyte
          • Defresult
          • Defsubtype
          • Pos-list
          • Defflatsum
          • Deflist-of-len
          • Defbytelist
          • Defset
          • Specific-types
          • Defbyte-standard-instances
          • Deffixtype-alias
          • Defomap
          • Defbytelist-standard-instances
            • Ubyte8-list
            • Ubyte4-list
            • Ubyte32-list
            • Ubyte64-list
            • Ubyte3-list
            • Ubyte256-list
            • Ubyte2-list
            • Ubyte16-list
            • Ubyte128-list
            • Ubyte11-list
            • Ubyte1-list
            • Sbyte64-list
            • Sbyte32-list
            • Sbyte256-list
            • Sbyte16-list
            • Sbyte128-list
            • Sbyte8-list
            • Sbyte4-list
            • Sbyte3-list
            • Sbyte2-list
            • Sbyte1-list
            • Defubytelist
            • Defsbytelist
          • Defunit
          • Byte-list
          • Byte
          • Nibble
          • Pos-option
          • Nat-option
          • Byte-list20
          • String-option
          • Byte-list32
          • Byte-list64
          • Pseudo-event-form
          • Character-list
          • Natoption/natoptionlist
          • Nati
          • Maybe-string
          • Nat/natlist
          • Nibble-list
          • Natoption/natoptionlist-result
          • Set
          • Nat/natlist-result
          • Nat-option-list-result
          • String-result
          • String-list-result
          • Nat-result
          • Nat-option-result
          • Nat-list-result
          • Maybe-string-result
          • Integer-result
          • Character-result
          • Character-list-result
          • Boolean-result
          • Map
          • Bag
          • Pseudo-event-form-list
          • Nat-option-list
          • Nat-set
          • Bit-list
        • Isar
        • Kestrel-utilities
        • Prime-field-constraint-systems
        • Soft
        • Bv
        • Imp-language
        • Event-macros
        • Bitcoin
        • Ethereum
        • Yul
        • Zcash
        • ACL2-programming-language
        • Prime-fields
        • Java
        • C
        • Syntheto
        • Number-theory
        • Cryptography
        • Lists-light
        • File-io-light
        • Json
        • Built-ins
        • Solidity
        • Axe
        • Std-extensions
        • Htclient
        • Typed-lists-light
        • Arithmetic-light
      • X86isa
      • Execloader
      • Axe
    • Testing-utilities
    • Math
  • Fty-extensions
  • Specific-types
  • Defbytelist

Defbytelist-standard-instances

Standard fixtypes of true lists of unsigned and signed bytes of various sizes, with some accompanying theorems.

Here `standard' means that these all have uniform structure and naming. They are unary counterparts of (unsigned-byte-listp n ...) and (signed-byte-listp n ...), for various values of n.

These are all generated via defbytelist.

If standard (in the sense above) fixtypes of true lists of unsigned or signed bytes of a certain size are needed but are not among the ones defined here, they can be added here.

These fixtypes are based on the standard fixtypes of unsigned and signed bytes of various sizes that correspond to the element types of the lists.

Subtopics

Ubyte8-list
Fixtype of true lists of unsigned bytes of size 8.
Ubyte4-list
Fixtype of true lists of unsigned bytes of size 4.
Ubyte32-list
Fixtype of true lists of unsigned bytes of size 32.
Ubyte64-list
Fixtype of true lists of unsigned bytes of size 64.
Ubyte3-list
Fixtype of true lists of unsigned bytes of size 3.
Ubyte256-list
Fixtype of true lists of unsigned bytes of size 256.
Ubyte2-list
Fixtype of true lists of unsigned bytes of size 2.
Ubyte16-list
Fixtype of true lists of unsigned bytes of size 16.
Ubyte128-list
Fixtype of true lists of unsigned bytes of size 128.
Ubyte11-list
Fixtype of true lists of unsigned bytes of size 11.
Ubyte1-list
Fixtype of true lists of unsigned bytes of size 1.
Sbyte64-list
Fixtype of true lists of signed bytes of size 64.
Sbyte32-list
Fixtype of true lists of signed bytes of size 32.
Sbyte256-list
Fixtype of true lists of signed bytes of size 256.
Sbyte16-list
Fixtype of true lists of signed bytes of size 16.
Sbyte128-list
Fixtype of true lists of signed bytes of size 128.
Sbyte8-list
Fixtype of true lists of signed bytes of size 8.
Sbyte4-list
Fixtype of true lists of signed bytes of size 4.
Sbyte3-list
Fixtype of true lists of signed bytes of size 3.
Sbyte2-list
Fixtype of true lists of signed bytes of size 2.
Sbyte1-list
Fixtype of true lists of signed bytes of size 1.
Defubytelist
Specialized form of defbytelist for generating standard fixtypes of true lists of unsigned bytes of explicit integer sizes.
Defsbytelist
Specialized form of defbytelist for generating standard fixtypes of true lists of signed bytes of explicit integer sizes.