Collect all the function names that occur in an vl-atomlist-p and return them as a string list.
(vl-atomlist-collect-funnames x) → ans
Function:
(defun vl-atomlist-collect-funnames (x) (declare (xargs :guard (vl-exprlist-p x))) (declare (xargs :guard (vl-atomlist-p x))) (let ((__function__ 'vl-atomlist-collect-funnames)) (declare (ignorable __function__)) (b* (((when (atom x)) nil) (guts (vl-atom->guts (car x))) ((when (vl-fast-funname-p guts)) (cons (string-fix (vl-funname->name guts)) (vl-atomlist-collect-funnames (cdr x))))) (vl-atomlist-collect-funnames (cdr x)))))
Theorem:
(defthm string-listp-of-vl-atomlist-collect-funnames (b* ((ans (vl-atomlist-collect-funnames x))) (string-listp ans)) :rule-classes :rewrite)
Theorem:
(defthm vl-atomlist-collect-funnames-of-vl-exprlist-fix-x (equal (vl-atomlist-collect-funnames (vl-exprlist-fix x)) (vl-atomlist-collect-funnames x)))
Theorem:
(defthm vl-atomlist-collect-funnames-vl-exprlist-equiv-congruence-on-x (implies (vl-exprlist-equiv x x-equiv) (equal (vl-atomlist-collect-funnames x) (vl-atomlist-collect-funnames x-equiv))) :rule-classes :congruence)