		Search-engine friendly clone of the ACL2 documentation.

Binary-integer-literals

Bindig/uscores-to-digits

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

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

Any underscores in a binary-numeral in the grammar are just used for separation. This function returns the underlying sequence of binary digits, exluding also the prefix of the binary-numeral.

Definitions and Theorems

Function: bindig/uscores-to-digits

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

Theorem: bin-digit-listp-of-bindig/uscores-to-digits

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

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

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

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

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