Associate all comments with their modules/interfaces/etc.
(vl-descriptionlist-inject-comments x comment-map) → new-x
Function:
(defun vl-descriptionlist-inject-comments (x comment-map) (declare (xargs :guard (and (vl-descriptionlist-p x) (vl-commentmap-p comment-map)))) (let ((__function__ 'vl-descriptionlist-inject-comments)) (declare (ignorable __function__)) (b* ((comment-map (mergesort comment-map)) (fal (vl-commentmap-fal comment-map)) (ret (vl-descriptionlist-inject-comments-aux x fal x))) (fast-alist-free fal) ret)))
Theorem:
(defthm vl-descriptionlist-p-of-vl-descriptionlist-inject-comments (b* ((new-x (vl-descriptionlist-inject-comments x comment-map))) (vl-descriptionlist-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm vl-descriptionlist->names-of-vl-descriptionlist-inject-comments (equal (vl-descriptionlist->names (vl-descriptionlist-inject-comments x comment-map)) (vl-descriptionlist->names x)))