		Search-engine friendly clone of the ACL2 documentation.

Bits/bytes-digit-grouping

Bebytes=>bits

Ungroup bytes into bits, big-endian.

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

Definitions and Theorems

Function: bebytes=>bits

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

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

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

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

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

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

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