		Search-engine friendly clone of the ACL2 documentation.

Vl-gather-comments-fal

Vl-gather-comments-fal-nrev

Signature
(vl-gather-comments-fal-nrev minl maxl n min max fal nrev) → nrev
Arguments: minl — Guard (natp minl).; maxl — Guard (natp maxl).; n — Guard (natp n).; min — Guard (vl-location-p min).; max — Guard (vl-location-p max).; fal — Guard (vl-commentmap-falp fal).

Definitions and Theorems

Function: vl-gather-comments-fal-nrev

(defun vl-gather-comments-fal-nrev (minl maxl n min max fal nrev)
 (declare (xargs :stobjs (nrev)))
 (declare (xargs :guard (and (natp minl)
                             (natp maxl)
                             (natp n)
                             (vl-location-p min)
                             (vl-location-p max)
                             (vl-commentmap-falp fal))))
 (declare (xargs :guard (and (eql (vl-location->line min) minl)
                             (eql (vl-location->line max) maxl)
                             (<= minl n)
                             (<= n maxl))))
 (let ((__function__ 'vl-gather-comments-fal-nrev))
   (declare (ignorable __function__))
   (b* ((entry (hons-get n fal))
        (nrev (if entry (vl-gather-comments-nrev min max (cdr entry)
                                                 nrev)
                nrev))
        ((when (mbe :logic (zp (- (nfix n) (nfix minl)))
                    :exec (eql n minl)))
         (nrev-fix nrev)))
     (vl-gather-comments-fal-nrev minl maxl (- n 1)
                                  min max fal nrev))))

Theorem: vl-commentmap-p-of-vl-gather-comments-fal-nrev

(defthm vl-commentmap-p-of-vl-gather-comments-fal-nrev
 (implies
  (and (vl-commentmap-p nrev)
       (vl-commentmap-falp fal))
  (vl-commentmap-p
       (vl-gather-comments-fal-nrev minl maxl n min max fal nrev))))