		Search-engine friendly clone of the ACL2 documentation.

Digits-any-base

Nat=>lendian+

Convert a natural number to its non-empty minimum-length little-endian list of digits.

Signature
(nat=>lendian+ base nat) → digits
Arguments: base — Guard (dab-basep base).; nat — Guard (natp nat).
Returns: digits — Type (dab-digit-listp base digits).

The resulting list is never empty; it is (0) if nat is 0. The + in the name of this function can be read as `one or more' (as in typical regular expression notation).

See also nat=>lendian* and nat=>lendian.

Definitions and Theorems

Function: nat=>lendian+

(defun nat=>lendian+ (base nat)
  (declare (xargs :guard (and (dab-basep base) (natp nat))))
  (let ((__function__ 'nat=>lendian+))
    (declare (ignorable __function__))
    (b* ((digits (nat=>lendian* base nat)))
      (or digits (list 0)))))

Theorem: return-type-of-nat=>lendian+

(defthm return-type-of-nat=>lendian+
  (b* ((digits (nat=>lendian+ base nat)))
    (dab-digit-listp base digits))
  :rule-classes :rewrite)

Theorem: nat-listp-of-nat=>lendian+

(defthm nat-listp-of-nat=>lendian+
  (b* ((digits (nat=>lendian+ base nat)))
    (nat-listp digits))
  :rule-classes :rewrite)

Theorem: nat=>lendian+-of-0

(defthm nat=>lendian+-of-0
  (equal (nat=>lendian+ base 0) (list 0)))

Theorem: nat=>lendian+-of-dab-base-fix-base

(defthm nat=>lendian+-of-dab-base-fix-base
  (equal (nat=>lendian+ (dab-base-fix base) nat)
         (nat=>lendian+ base nat)))

Theorem: nat=>lendian+-dab-base-equiv-congruence-on-base

(defthm nat=>lendian+-dab-base-equiv-congruence-on-base
  (implies (dab-base-equiv base base-equiv)
           (equal (nat=>lendian+ base nat)
                  (nat=>lendian+ base-equiv nat)))
  :rule-classes :congruence)

Theorem: nat=>lendian+-of-nfix-nat

(defthm nat=>lendian+-of-nfix-nat
  (equal (nat=>lendian+ base (nfix nat))
         (nat=>lendian+ base nat)))

Theorem: nat=>lendian+-nat-equiv-congruence-on-nat

(defthm nat=>lendian+-nat-equiv-congruence-on-nat
  (implies (nat-equiv nat nat-equiv)
           (equal (nat=>lendian+ base nat)
                  (nat=>lendian+ base nat-equiv)))
  :rule-classes :congruence)