		Search-engine friendly clone of the ACL2 documentation.

Vl-gather-comments

Vl-gather-comments-nrev

Signature
(vl-gather-comments-nrev min max cmap nrev) → nrev
Arguments: min — Guard (vl-location-p min).; max — Guard (vl-location-p max).; cmap — Guard (vl-commentmap-p cmap).

Definitions and Theorems

Function: vl-gather-comments-nrev

(defun vl-gather-comments-nrev (min max cmap nrev)
  (declare (xargs :stobjs (nrev)))
  (declare (xargs :guard (and (vl-location-p min)
                              (vl-location-p max)
                              (vl-commentmap-p cmap))))
  (let ((__function__ 'vl-gather-comments-nrev))
    (declare (ignorable __function__))
    (b* (((when (atom cmap)) (nrev-fix nrev))
         (nrev (if (vl-location-between-p (caar cmap)
                                          min max)
                   (nrev-push (car cmap) nrev)
                 nrev)))
      (vl-gather-comments-nrev min max (cdr cmap)
                               nrev))))