		Search-engine friendly clone of the ACL2 documentation.

Vl-server

Vls-make-scannedalist

Signature
(vls-make-scannedalist x) → alist
Arguments: x — Guard (vl-zipinfolist-p x).
Returns: alist — Type (vls-scannedalist-p alist).

Definitions and Theorems

Function: vls-make-scannedalist

(defun vls-make-scannedalist (x)
  (declare (xargs :guard (vl-zipinfolist-p x)))
  (let ((__function__ 'vls-make-scannedalist))
    (declare (ignorable __function__))
    (if (atom x)
        nil
      (cons (cons (vl-zipinfo->filename (car x))
                  (vl-zipinfo-fix (car x)))
            (vls-make-scannedalist (cdr x))))))

Theorem: vls-scannedalist-p-of-vls-make-scannedalist

(defthm vls-scannedalist-p-of-vls-make-scannedalist
  (b* ((alist (vls-make-scannedalist x)))
    (vls-scannedalist-p alist))
  :rule-classes :rewrite)