		Search-engine friendly clone of the ACL2 documentation.

Vl-commentmap-fal

Vl-commentmap-fal-aux

Construct the vl-commentmap-falp for a vl-commentmap-p.

Signature
(vl-commentmap-fal-aux x alist) → *
Arguments: x — Commentmap we're processing.
Guard (vl-commentmap-p x).; alist — The fast alist we're extending.

Definitions and Theorems

Function: vl-commentmap-fal-aux

(defun vl-commentmap-fal-aux (x alist)
  (declare (xargs :guard (vl-commentmap-p x)))
  (let ((__function__ 'vl-commentmap-fal-aux))
    (declare (ignorable __function__))
    (b* (((when (atom x)) alist)
         (line (vl-location->line (caar x)))
         (curr (cdr (hons-get line alist)))
         (alist (hons-acons line (cons (car x) curr)
                            alist)))
      (vl-commentmap-fal-aux (cdr x) alist))))

Theorem: consp-of-vl-commentmap-fal-aux

(defthm consp-of-vl-commentmap-fal-aux
  (equal (consp (vl-commentmap-fal-aux x alist))
         (or (consp alist) (consp x))))

Theorem: vl-commentmap-falp-of-vl-commentmap-fal-aux

(defthm vl-commentmap-falp-of-vl-commentmap-fal-aux
  (implies (and (vl-commentmap-p x)
                (vl-commentmap-falp alist))
           (vl-commentmap-falp (vl-commentmap-fal-aux x alist))))