		Search-engine friendly clone of the ACL2 documentation.

Bits-as-digits-in-base-2

Lebits=>nat

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

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

Definitions and Theorems

Function: lebits=>nat

(defun lebits=>nat (digits)
  (declare (xargs :guard (bit-listp digits)))
  (let ((__function__ 'lebits=>nat))
    (declare (ignorable __function__))
    (lendian=>nat 2 digits)))

Theorem: natp-of-lebits=>nat

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

Theorem: lebits=>nat-of-bit-list-fix-digits

(defthm lebits=>nat-of-bit-list-fix-digits
  (equal (lebits=>nat (bit-list-fix digits))
         (lebits=>nat digits)))

Theorem: lebits=>nat-bit-list-equiv-congruence-on-digits

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

Subtopics

Lebits=>nat-injectivity+
Lebits=>nat-injectivity*
Lebits=>nat-injectivity
Nat=>lebits+-of-lebits=>nat
Nat=>lebits*-of-lebits=>nat
Nat=>lebits-of-lebits=>nat
Lebits=>nat-of-nat=>lebits+
Lebits=>nat-of-nat=>lebits*
Lebits=>nat-of-nat=>lebits