		Search-engine friendly clone of the ACL2 documentation.

Vl-commentmap-falp

Vl-commentmap-lines-agreep

Signature
(vl-commentmap-lines-agreep line x) → *
Arguments: line — Guard (posp line).; x — Guard (vl-commentmap-p x).

Definitions and Theorems

Function: vl-commentmap-lines-agreep

(defun vl-commentmap-lines-agreep (line x)
  (declare (xargs :guard (and (posp line) (vl-commentmap-p x))))
  (let ((__function__ 'vl-commentmap-lines-agreep))
    (declare (ignorable __function__))
    (if (atom x)
        t
      (and (equal (vl-location->line (caar x))
                  line)
           (vl-commentmap-lines-agreep line (cdr x))))))

Theorem: vl-commentmap-lines-agreep-when-not-consp

(defthm vl-commentmap-lines-agreep-when-not-consp
  (implies (not (consp x))
           (equal (vl-commentmap-lines-agreep line x)
                  t)))

Theorem: vl-commentmap-lines-agreep-of-cons

(defthm vl-commentmap-lines-agreep-of-cons
  (equal (vl-commentmap-lines-agreep line (cons a x))
         (and (equal (vl-location->line (car a)) line)
              (vl-commentmap-lines-agreep line x))))