		Search-engine friendly clone of the ACL2 documentation.

Octal-integer-literals

Octdig/uscores-to-digits

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

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

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

Definitions and Theorems

Function: octdig/uscores-to-digits

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

Theorem: oct-digit-listp-of-octdig/uscores-to-digits

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

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

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

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

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