		Search-engine friendly clone of the ACL2 documentation.

Bytes-as-digits-in-base-256

Lebytes=>nat

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

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

Definitions and Theorems

Function: lebytes=>nat

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

Theorem: natp-of-lebytes=>nat

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

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

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

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

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

Subtopics

Lebytes=>nat-injectivity+
Lebytes=>nat-injectivity*
Lebytes=>nat-injectivity
Nat=>lebytes+-of-lebytes=>nat
Nat=>lebytes*-of-lebytes=>nat
Nat=>lebytes-of-lebytes=>nat
Lebytes=>nat-of-nat=>lebytes+
Lebytes=>nat-of-nat=>lebytes*
Lebytes=>nat-of-nat=>lebytes