		Search-engine friendly clone of the ACL2 documentation.

Vl-commentmap-p

Vl-gather-comments-fal

Efficient routine for gathering comments using an vl-commentmap-falp.

Signature
(vl-gather-comments-fal min max fal) → *
Arguments: 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

(defun vl-gather-comments-fal (min max fal)
  (declare (xargs :guard (and (vl-location-p min)
                              (vl-location-p max)
                              (vl-commentmap-falp fal))))
  (declare (xargs :guard (<= (vl-location->line min)
                             (vl-location->line max))))
  (let ((__function__ 'vl-gather-comments-fal))
    (declare (ignorable __function__))
    (b* ((minl (vl-location->line min))
         (maxl (vl-location->line max)))
      (with-local-nrev (vl-gather-comments-fal-nrev
                            minl maxl maxl min max fal nrev)))))

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

(defthm vl-commentmap-p-of-vl-gather-comments-fal
  (implies (force (vl-commentmap-falp fal))
           (vl-commentmap-p (vl-gather-comments-fal min max fal))))

Subtopics

Vl-gather-comments-fal-nrev