		Search-engine friendly clone of the ACL2 documentation.

Decimal-integer-literals

Decdig/uscores-to-digits

Remove the underscores from a list of decimal digits and underscores.

Signature
(decdig/uscores-to-digits dus) → ds
Arguments: dus — Guard (decdig/uscore-listp dus).
Returns: ds — Type (dec-digit-listp ds).

Any underscores in a decimal-numeral in the grammar are just used for separation. This function returns the underlying sequence of decimal digits.

Definitions and Theorems

Function: decdig/uscores-to-digits

(defun decdig/uscores-to-digits (dus)
  (declare (xargs :guard (decdig/uscore-listp dus)))
  (let ((__function__ 'decdig/uscores-to-digits))
    (declare (ignorable __function__))
    (b* (((when (endp dus)) nil) (du (car dus)))
      (decdig/uscore-case
           du
           :digit (cons du.get
                        (decdig/uscores-to-digits (cdr dus)))
           :underscore (decdig/uscores-to-digits (cdr dus))))))

Theorem: dec-digit-listp-of-decdig/uscores-to-digits

(defthm dec-digit-listp-of-decdig/uscores-to-digits
  (b* ((ds (decdig/uscores-to-digits dus)))
    (dec-digit-listp ds))
  :rule-classes :rewrite)

Theorem: decdig/uscores-to-digits-of-decdig/uscore-list-fix-dus

(defthm decdig/uscores-to-digits-of-decdig/uscore-list-fix-dus
  (equal (decdig/uscores-to-digits (decdig/uscore-list-fix dus))
         (decdig/uscores-to-digits dus)))

Theorem: decdig/uscores-to-digits-decdig/uscore-list-equiv-congruence-on-dus

(defthm
 decdig/uscores-to-digits-decdig/uscore-list-equiv-congruence-on-dus
 (implies (decdig/uscore-list-equiv dus dus-equiv)
          (equal (decdig/uscores-to-digits dus)
                 (decdig/uscores-to-digits dus-equiv)))
 :rule-classes :congruence)