		Search-engine friendly clone of the ACL2 documentation.

Bits/bytes-digit-grouping

Bits=>lebytes

Group bits into bytes, little-endian.

Signature
(bits=>lebytes digits) → new-digits
Arguments: digits — Guard (bit-listp digits).
Returns: new-digits — Type (byte-listp new-digits).

Definitions and Theorems

Function: bits=>lebytes

(defun bits=>lebytes (digits)
  (declare (xargs :guard (bit-listp digits)))
  (declare (xargs :guard (integerp (/ (len digits) 8))))
  (let ((__function__ 'bits=>lebytes))
    (declare (ignorable __function__))
    (group-lendian 2 8 digits)))

Theorem: byte-listp-of-bits=>lebytes

(defthm byte-listp-of-bits=>lebytes
  (b* ((new-digits (bits=>lebytes digits)))
    (byte-listp new-digits))
  :rule-classes :rewrite)

Theorem: bits=>lebytes-of-bit-list-fix-digits

(defthm bits=>lebytes-of-bit-list-fix-digits
  (equal (bits=>lebytes (bit-list-fix digits))
         (bits=>lebytes digits)))

Theorem: bits=>lebytes-bit-list-equiv-congruence-on-digits

(defthm bits=>lebytes-bit-list-equiv-congruence-on-digits
  (implies (bit-list-equiv digits digits-equiv)
           (equal (bits=>lebytes digits)
                  (bits=>lebytes digits-equiv)))
  :rule-classes :congruence)