		Search-engine friendly clone of the ACL2 documentation.

Lexer-utils

Vl-echarlist-kill-underscores

Remove all occurrences of the underscore character from a vl-echarlist-p.

Signature
(vl-echarlist-kill-underscores x) → reduced-x
Arguments: x — Guard (vl-echarlist-p x).
Returns: reduced-x — Type (vl-echarlist-p reduced-x), given the guard.

Verilog uses underscores as a digit separator, e.g., you can write 1_000_000 instead of 1000000 for greater readability on long numbers. This function strips away the underscores so we can interpret the remaining digits with vl-echarlist-unsigned-value.

Definitions and Theorems

Function: vl-echarlist-kill-underscores

(defun vl-echarlist-kill-underscores (x)
  (declare (xargs :guard (vl-echarlist-p x)))
  (let ((__function__ 'vl-echarlist-kill-underscores))
    (declare (ignorable __function__))
    (cond ((atom x) nil)
          ((eql (vl-echar->char (car x)) #\_)
           (vl-echarlist-kill-underscores (cdr x)))
          (t (cons (car x)
                   (vl-echarlist-kill-underscores (cdr x)))))))

Theorem: vl-echarlist-p-of-vl-echarlist-kill-underscores

(defthm vl-echarlist-p-of-vl-echarlist-kill-underscores
  (implies (and (force (vl-echarlist-p x)))
           (b* ((reduced-x (vl-echarlist-kill-underscores x)))
             (vl-echarlist-p reduced-x)))
  :rule-classes :rewrite)