Remove all occurrences of the underscore character from a vl-echarlist-p.
(vl-echarlist-kill-underscores x) → reduced-x
Verilog uses underscores as a digit separator, e.g., you can write
Function:
(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:
(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)