		Search-engine friendly clone of the ACL2 documentation.

Bits/bytes-digit-grouping

Lebytes=>bits

Ungroup bytes into bits, little-endian.

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

Definitions and Theorems

Function: lebytes=>bits

(defun lebytes=>bits (digits)
  (declare (xargs :guard (byte-listp digits)))
  (let ((__function__ 'lebytes=>bits))
    (declare (ignorable __function__))
    (ungroup-lendian 2 8 digits)))

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

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

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

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

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

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