		Search-engine friendly clone of the ACL2 documentation.

Byte-list

A fixtype of true lists of (unsigned 8-bit) bytes.

We use fty::defbytelist to generate this fixtype, along with the recognizer, fixer, and equivalence.

Theorem: byte-listp-forward-unsigned-byte-listp

(defthm byte-listp-forward-unsigned-byte-listp
        (implies (byte-listp x)
                 (unsigned-byte-listp 8 x))
        :rule-classes :forward-chaining)

Theorem: byte-listp-rewrite-unsigned-byte-listp

(defthm byte-listp-rewrite-unsigned-byte-listp
        (equal (byte-listp x)
               (unsigned-byte-listp 8 x)))

Theorem: unsigned-byte-listp-rewrite-byte-listp

(defthm unsigned-byte-listp-rewrite-byte-listp
        (equal (unsigned-byte-listp 8 x)
               (byte-listp x)))

Theorem: true-listp-when-byte-listp-rewrite

(defthm true-listp-when-byte-listp-rewrite
        (implies (byte-listp x) (true-listp x)))

Theorem: byte-list-fix-of-take

(defthm byte-list-fix-of-take
        (implies (<= (nfix n) (len x))
                 (equal (byte-list-fix (take n x))
                        (take n (byte-list-fix x)))))

Theorem: byte-list-fix-of-rcons

(defthm byte-list-fix-of-rcons
        (equal (byte-list-fix (rcons a x))
               (rcons (byte-fix a) (byte-list-fix x))))

Subtopics

Byte-listp: (byte-listp x) recognizes lists where every element satisfies bytep.
Byte-list-fix: (byte-list-fix x) is a usual fty list fixing function.
Byte-list20: A fixtype of true lists of (unsigned 8-bit) bytes of length 20.
Byte-list32: A fixtype of true lists of (unsigned 8-bit) bytes of length 32.
Byte-list64: A fixtype of true lists of (unsigned 8-bit) bytes of length 64.
Byte-list-equiv: Basic equivalence relation for byte-list structures.