		Search-engine friendly clone of the ACL2 documentation.

Bytes-as-digits-in-base-256

Bebytes=>nat

Convert a big-endian list of bytes, seen as digits in base 256, to their value.

Signature
(bebytes=>nat digits) → nat
Arguments: digits — Guard (byte-listp digits).
Returns: nat — Type (natp nat).

Definitions and Theorems

Function: bebytes=>nat

(defun bebytes=>nat (digits)
  (declare (xargs :guard (byte-listp digits)))
  (let ((__function__ 'bebytes=>nat))
    (declare (ignorable __function__))
    (bendian=>nat 256 digits)))

Theorem: natp-of-bebytes=>nat

(defthm natp-of-bebytes=>nat
  (b* ((nat (bebytes=>nat digits)))
    (natp nat))
  :rule-classes :rewrite)

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

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

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

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

Subtopics

Bebytes=>nat-injectivity+
Bebytes=>nat-injectivity*
Bebytes=>nat-injectivity
Nat=>bebytes+-of-bebytes=>nat
Nat=>bebytes*-of-bebytes=>nat
Nat=>bebytes-of-bebytes=>nat
Bebytes=>nat-of-nat=>bebytes+
Bebytes=>nat-of-nat=>bebytes*
Bebytes=>nat-of-nat=>bebytes