		Search-engine friendly clone of the ACL2 documentation.

Nibble-list

A fixtype of true lists of (unsigned 4-bit) nibbles.

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

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

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

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

(defthm nibble-listp-rewrite-unsigned-byte-listp
  (equal (nibble-listp x)
         (unsigned-byte-listp 4 x)))

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

(defthm unsigned-byte-listp-rewrite-nibble-listp
  (equal (unsigned-byte-listp 4 x)
         (nibble-listp x)))

Theorem: true-listp-when-nibble-listp-rewrite

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

Theorem: nibble-list-fix-of-take

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

Theorem: nibble-list-fix-of-rcons

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

Subtopics

Nibble-list-fix: (nibble-list-fix x) is a usual fty list fixing function.
Nibble-list-equiv: Basic equivalence relation for nibble-list structures.
Nibble-listp: (nibble-listp x) recognizes lists where every element satisfies nibblep.